diff options
| -rw-r--r-- | README.md | 10 | ||||
| -rw-r--r-- | USE.md | 15 |
2 files changed, 21 insertions, 4 deletions
@@ -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, @@ -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 |