Bill Allombert on Mon, 12 May 2014 14:14:27 +0200

[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]

GIT repository reset

Dear PARI developers,

Due to an accidental push of an empty merger commit,
I had to reset the git repository.

The official GIT should include the commit

If it is not the case, assuming you do not have changes, you can do
git checkout master
git reset --hard origin/master

Sorry for the trouble.