Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Question about EXTRA_OPAM_OPTION / EXTRA_FLAGS #1499

Closed
erikmd opened this issue Dec 7, 2020 · 4 comments
Closed

Question about EXTRA_OPAM_OPTION / EXTRA_FLAGS #1499

erikmd opened this issue Dec 7, 2020 · 4 comments

Comments

@erikmd
Copy link
Member

erikmd commented Dec 7, 2020

Cc @palmskog @gares

By taking a look at #1498, I saw there's an EXTRA_OPAM_OPTION variable in .gitlab-ci.yml:
https://github.com/coq/opam-coq-archive/blob/b258b1194d5109d28f1b516020b777a18a8a32d0/.gitlab-ci.yml#L122
but I am puzzled to see that this variable does not seem to be used; there is only EXTRA_FLAGS :
https://github.com/coq/opam-coq-archive/blob/e1fb37fbf6ebaacbe1e446223d7b2f052b2cc222/scripts/opam-coq-init#L10
Should one of these variables be renamed to the other?

Sorry if I missed something and the code is OK actually.

@gares
Copy link
Member

gares commented Dec 7, 2020

I don't know sorry

@palmskog
Copy link
Contributor

palmskog commented Dec 8, 2020

No precise idea here either. It may be some remnant from the OPAM 1 days.

@clarus
Copy link
Contributor

clarus commented Apr 22, 2021

This option appears in https://github.com/coq/opam-coq-archive/blob/master/scripts/opam-coq-install-remove :

echo Check if $PKG_NAME_VERSION is installable
if opam install "$PKG_NAME_VERSION" -y --show-action $EXTRA_OPAM_OPTION; then
  set +e
  echo Installing $PKG_NAME_VERSION
  opam install "$PKG_NAME_VERSION" -y -v -v --with-test $EXTRA_OPAM_OPTION >> $LOG

I added that for the target any in order to test the install with whatever OCaml compiler fits. Does that answer your remark?

@erikmd
Copy link
Member Author

erikmd commented Apr 24, 2021

Hi @clarus, yes, definitely! thanks for your feedback :)

@erikmd erikmd closed this as completed Apr 24, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants