Really report repository ids

And make the script for that available.

Closes: #11 (closed)

mentioned in issue #13 (closed)

added 1 commit

• 8767b481 - Really report repository ids

Compare with previous version

added 1 commit

• d71794f6 - Really report repository ids

Compare with previous version

OK, I think I've done what I can here. But there is a problem that for the wrapper repos I do not get the git information of the wrapped repos, as that .git of the wrapper repo remains, and only the contents of the wrapped repo is moved up.

enabled an automatic merge when the pipeline for d71794f6 succeeds

merged

mentioned in commit 082fcfb8

Raised the inconsistency issue:

• https://zivgitlab.uni-muenster.de/HPC2SE-Project/pacxx-rv2/issues/1
• https://zivgitlab.uni-muenster.de/HPC2SE-Project/pacxx-llvm2/issues/1