Follow-up Comment #2, sr #110321 (project administration):
Thanks, that's great! Indeed, I understand both reasons; as you noted, the
code mistakenly pushed to master is indeed available on the "vala" branch; and
as for the secondary reason, it's precisely to avoid the mistakenly-pushed
commit becoming integrated into the history of downstream users that I wanted
to remove it pronto.
Do please close the issue now, and thanks again for your help.
_______________________________________________________
Reply to this item at:
<https://savannah.nongnu.org/support/?110321>
_______________________________________________
Message sent via Savannah
https://savannah.nongnu.org/
