diff options
| author | Ewout ter Hoeven <E.M.terHoeven@student.tudelft.nl> | 2024-04-04 17:08:55 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2024-04-04 17:08:55 +0200 |
| commit | c666ba26c39d5c07e07b4e1e411332f408e309ad (patch) | |
| tree | e73e4698ef175e0ccca3df3b6b54d06e5faa84ef /scripts/ci-run.sh | |
| parent | 2e66913e5f56209f4c949f98e431925b78e7e84d (diff) | |
build CI: Name artifacts (#6482)
Name the artifacts in the build CI, so that they get uploaded with separate names, instead of all put into the same `artifact` ZIP.
It might be possible to further simplify the packing step (in future PRs).
Diffstat (limited to 'scripts/ci-run.sh')
0 files changed, 0 insertions, 0 deletions