packages missing in github mirror

Elan Ruusamäe glen at
Mon May 9 15:24:24 CEST 2022

On 04.05.2022 15:21, Jan Palus wrote:

> It appears that some packages are not mirrored to github.
> Completely missing or tree empty (some of them missing due to notorious
> dns issues):

synced some of them with:

[~/relup] ➔ for a in `cat /tmp/pkgs `; do (./builder -g -ns $a && cd $a 
&& git co -b hg-temp-mirror && git push -u origin hg-temp-mirror && cd 
..); done
[~/relup] ➔ for a in `cat /tmp/pkgs `; do (cd $a && git push -u origin 
--delete hg-temp-mirror && cd ..); done

some got error:
remote: fatal: Could not read from remote repository.

this one is weird, it had no HEAD before?

remote: To ssh://
remote:  ! [remote rejected] hg-temp-mirror (refusing to delete the 
current branch: refs/heads/hg-temp-mirror)
remote: error: failed to push some refs to 
remote: ...done

More information about the pld-devel-en mailing list