Since we were talking about setting up actual push permissions when moving to github, I've drafted a "process with github" document.
PLEASE REVIEW It will of course need to be updated as we go with it, but it is important to have a consensus on at least the first version ... http://rock.opendfki.de/wiki/WikiStart/Standards/RG9 Sylvain
_______________________________________________ Rock-dev mailing list [email protected] http://www.dfki.de/mailman/cgi-bin/listinfo/rock-dev
