path: root/USE.md
diff options
authorJonas Smedegaard <dr@jones.dk>2021-06-04 15:13:48 +0200
committerJonas Smedegaard <dr@jones.dk>2021-06-04 15:13:48 +0200
commited4f13b2367a6a9f2054edd4b1974419ba338ca9 (patch)
tree54515a961a272578c59fd3b86b4d28e759b369d7 /USE.md
parent07df086f5de0ae840e857a58f00c743ad7536e11 (diff)
use inline defined hints
Diffstat (limited to 'USE.md')
1 files changed, 12 insertions, 3 deletions
diff --git a/USE.md b/USE.md
index d9459b1..2e5241e 100644
--- a/USE.md
+++ b/USE.md
@@ -5,6 +5,15 @@
> -- a [pun][UTSL] on Obi-Wan Kenobi quote in Star Wars
+## Special strings
+NB! This documentation uses special strings
+which you may want to adapt for your local setup:
+githost: source.example.org
+gitshellhost: git.example.org
## Git
Digital source material is tracked with git.
@@ -47,7 +56,7 @@ in one go:
To collaborate on a shared git repository,
first create a local copy from the shared location:
- git clone git://{{githost}}/example
+ git clone git://source.example.org/example
Then from time to time syncronize,
first fetch eventual updates from others
@@ -63,8 +72,8 @@ first create a new empty git publicly,
then tell your local git where its new origin will be,
and finally push your local git into its new public location:
- ssh {{gitshellhost}} git init --bare --shared /srv/git/{{githost}}/example.git
- git remote add origin {{gitshellhost}}:/srv/git/{{githost}}/example.git
+ ssh git.example.org git init --bare --shared /srv/git/source.example.org/example.git
+ git remote add origin git.example.org:/srv/git/source.example.org/example.git
git push --set-upstream origin master