Correct git config for end-of-line characters. Linux and Windows need different settings

rcasero committed Jul 11, 2016

repository moved from rcasero account to vigente organization account

rcasero committed Jul 10, 2016

Everybody uses core.autocrlf true to avoid problems with EOL characters changing

rcasero committed Jul 6, 2016

simplify instructions

rcasero committed May 26, 2016

fix links for Windows users

rcasero committed May 25, 2016

use "origin" instead of "gerardus" as remote

rcasero committed May 25, 2016

delete details about admin stuff, and make USERNAME more visible in remote add

foxu2798 committed May 25, 2016

minor

rcasero committed Nov 5, 2015

if you include your username in "git remote add...", then they don't ask you for it every time you push

rcasero committed Nov 5, 2015

Add link to public mailing list

rcasero committed Nov 3, 2015

add name of private repository

rcasero committed Jul 17, 2015

add how to delete a branch on github server

BenVillard committed May 26, 2015

add instructions for accessing sombody else's branch

ck3294 committed May 7, 2015

Minor

rcasero committed Apr 30, 2015

Make clear that the "papers-public" directory has to be outside of the "gerardus" directory. Pointed out by Jo

rcasero committed Apr 30, 2015

add section "Downloading ("cloning") the papers directory to your computer"

rcasero committed Apr 28, 2015

Basics about how to get working with gerardus using github

rcasero committed Apr 27, 2015