aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--README.md10
-rw-r--r--USE.md15
2 files changed, 21 insertions, 4 deletions
diff --git a/README.md b/README.md
index 96f96ab..8a3d66e 100644
--- a/README.md
+++ b/README.md
@@ -3,6 +3,14 @@
Digital source material.
+## Special strings
+
+NB! This documentation uses special strings
+which you may want to adapt for your local setup:
+
+githost: source.example.org
+
+
## Git
Digital source material is tracked with git.
@@ -14,7 +22,7 @@ a repository for historic versions of file contents of a folder.
## Collections
A collection of public git repositories is available
-at <https://{{githost}}/>.
+at <https://source.example.org/>.
Additional git repositories,
public or accessible only by a smaller group,
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