Skip to content

Commit

Permalink
Fix repository index generation
Browse files Browse the repository at this point in the history
The existing script was too ad-hoc.
  • Loading branch information
maximedenes committed Aug 20, 2023
1 parent 6b1b873 commit b182781
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ jobs:
- name: Build index
run: |
eval $(opam env)
make
scripts/generate-opam-indexes released core-dev extra-dev
- name: Build JSON index data
run: |
Expand Down
13 changes: 13 additions & 0 deletions scripts/generate-opam-indexes
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
#!/bin/bash -e
#
# Script which generates the index for OPAM packages to be served through HTTP.
# Similar to refresh-opam-indexes, but less ad-hoc (no hardcoded paths & e-mail
# addresses) and better suited for use as part of a CI workflow

OPAMCHECKOPTS=--cycles

for repo in "$@"; do
cd "$repo"
opam admin check $OPAMCHECKOPTS && opam admin make
cd ..
done

0 comments on commit b182781

Please sign in to comment.