Thanks - this helps considerably. However, it's long on technical information on how one could work with git, and short on policy, i.e. how you want us to use git for PLT. Immediate questions:
- Should we merge or rebase? - Should we push directly to origin/master, or somewhere else, and you do the pulling? (Push doesn't scale indefinitely.) - For longer-lived branches that we want others to see, do you want us to use named branches within the main repo, or user repositories? -- Cheers =8-} Mike Friede, Völkerverständigung und überhaupt blabla _________________________________________________ For list-related administrative tasks: http://list.cs.brown.edu/mailman/listinfo/plt-dev
