collect at specific date
Hi, for my course I had to do the following to switch the student repo to a specific date after a collect (in particuler after en exam) :
git pull origin master
git -c advice.detachedHead=false checkout 'origin/HEAD@{date}'
instead of
git pull
git -c advice.detachedHead=false checkout 'master@{date}'
We might want to discuss this before I propose a commit. I had to it quickly a month ago and I don't remember why the master@{date} was not enough, but it wasn't. Any comment on this ?
Jérémy