Skip to content
Snippets Groups Projects
Commit 082fcfb8 authored by Jö Fahlke's avatar Jö Fahlke
Browse files

[!53] Really report repository ids 

Merge branch 'really-report-repo-ids' into 'master'

And make the script for that available.

Closes: [#11]

See merge request [joe/pacxx-docker!53]

  [#11]: gitlab.dune-project.org/joe/pacxx-docker/issues/11
  [joe/pacxx-docker!53]: gitlab.dune-project.org/joe/pacxx-docker/merge_requests/53


Closes #11
parents 417463ea d71794f6
No related branches found
No related tags found
1 merge request!53Really report repository ids
Pipeline #12301 canceled
Stage: utils
Stage: base
Stage: pacxx-source
Stage: pacxx-build
Stage: mkimage
Stage: test
Stage: deploy
Hide whitespace changes
Inline Side-by-side
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment