Hi,
Nigel Metheringham <nigel@???> (Do 07 Apr 2016 12:55:04 CEST):
> Hi,
>
> I've just had to unknot git a little bit - the HEAD commit on the github
> and hummus respositories were different versions of the same commit.
>
> I presume that Heiko had amended a commit that was previously pushed to
> one of the repos, and the periodic process that syncs the two repos
> could not determine which was the correct HEAD to use.
Yes, it was my fault.
commit
push
commit --amend
push --force
> Please could you check that I have ended up with the correct commit
> (03f68c52bd7d014304b03ad6394343350ea71b2c) as the top one, as both repos
> now use that commit.
…
> The difference between them was whether 0 or FALSE was used in the
> changed line.
Almost.
dns_init(0, 0)
vs
dns_init(FALSE, FALSE, FALSE);
The latter being the right one (03f68c52bd7d014304b03ad6394343350ea71b2c)
Sorry for the mess.
Best regards from Dresden/Germany
Viele Grüße aus Dresden
Heiko Schlittermann
--
SCHLITTERMANN.de ---------------------------- internet & unix support -
Heiko Schlittermann, Dipl.-Ing. (TU) - {fon,fax}: +49.351.802998{1,3} -
gnupg encrypted messages are welcome --------------- key ID: F69376CE -
! key id 7CBF764A and 972EAC9F are revoked since 2015-01 ------------ -
