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

Update coq-validsdp.dev #2316

Merged
merged 1 commit into from Sep 23, 2022
Merged

Update coq-validsdp.dev #2316

merged 1 commit into from Sep 23, 2022

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Sep 20, 2022

ci-skip: coq-libvalidsdp.dev

@silene
Copy link
Contributor

silene commented Sep 20, 2022

The line ci-skip:coq-libvalidsdp.1.0.1 should not be part of the commit messages (especially not the commit title). It should just be part of the pull request message (currently empty). Also, it should correspond to the version actually modified by the pull request, so here it would be ci-skip:coq-libvalidsdp.dev.

@proux01
Copy link
Contributor Author

proux01 commented Sep 20, 2022

@silene well, this still seems to first check coq-libvalidsdp.dev alone. In the log we find

SKIP packages per user request: ci-skip:coq-libvalidsdp.dev
[...]
Testing extra-dev/packages/coq-libvalidsdp/coq-libvalidsdp.dev/opam

BTW, definitely unrelated but what's that:

$ apt-get install libgtksourceview2.0-dev -y || true
Reading package lists...
Building dependency tree...
Reading state information...
E: Unable to locate package libgtksourceview2.0-dev
E: Couldn't find any package by glob 'libgtksourceview2.0-dev'
E: Couldn't find any package by regex 'libgtksourceview2.0-dev'

@silene
Copy link
Contributor

silene commented Sep 20, 2022

My mistake. You need to put a space after the colon. (This could definitely be improved.)

@palmskog
Copy link
Contributor

@proux01 doesn't look like the project is compatible with coq.dev due to lack of locality hints:

Error: The default value for instance locality is currently "local" in a
# section and "global" otherwise, but is scheduled to change in a future
# release.

Do you want to fix this or should I merge anyway? We have laxer standards for the extra-dev repo.

@proux01
Copy link
Contributor Author

proux01 commented Sep 20, 2022

Indeed, this is a relatively recent change in master, let us fix that in validsdp first.

@proux01
Copy link
Contributor Author

proux01 commented Sep 23, 2022

Upstream fixed, CI green

@palmskog palmskog merged commit d3cadc6 into coq:master Sep 23, 2022
@proux01 proux01 deleted the validsdp.dev branch September 23, 2022 08:21
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

Successfully merging this pull request may close these issues.

None yet

3 participants