Thorsten Jolitz <tjol...@gmail.com> writes: > Still not fixed, or an error on my side?
Your commit was well in the repository (i.e., well pushed.) I republished Org. What we do know is that the local version of Org is obtained with ~$ git checkout release_7.9.4 -- and there are some cron jobs which used to switch back again to the maint or master branch. Last time I fixed the scripts, this time I simply checked out release_7.9.4 again, as the org-mode repo was using the maint branch... I don't know why. Thanks for reporting this, -- Bastien
