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
ca2f47bcf845b22451cf9e5fd56f03c176e94412

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.

Cheers,
Bill.