On Apr 28, 2010, at 6:39 AM, Philippe Meunier wrote: > In fact it looks to me like, rather then going through a private copy > of the main repo that sits on the main git server, what I should > really do is have my own local public git server. Then I can use it > to synchronize things between machines locally, break any code I want, > pull new changes from the main repo whenever I want, and only push > from that server to the main repo when I'm ready. In other words, > move to a truly distributed system for which git was designed rather > than trying to shoe-horn git into something that looks like svn?
Right. The use of usr space on the PLT git server was mainly for those who don't have a machine with a public IP (or a private VPN) and thus need a machine they can access from anywhere. If you have such a machine, it's simple to set up. Even more so that you don't need to run anything special like a git server for it; you just need SSH access to your machine. (Before Eli set up the usr space, I used to do this on my lab machine, which does have a public IP. My computers at home cloned the repo that was there in ~/plt via the SSH method, and it worked well. I switched to the version above because I plan on coordinating with other people like Sam for projects, and I don't want to have to create new user accounts on my lab machine for each person with whom I want to work.) Stevie_________________________________________________ For list-related administrative tasks: http://list.cs.brown.edu/mailman/listinfo/plt-dev