8000 In gitlab set TRAVIS_BRANCH so user overlays will work as expected. by SkySkimmer · Pull Request #1065 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

In gitlab set TRAVIS_BRANCH so user overlays will work as expected. #1065

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Sep 22, 2017
Merged

In gitlab set TRAVIS_BRANCH so user overlays will work as expected. #1065

merged 1 commit into from
Sep 22, 2017

Conversation

SkySkimmer
Copy link
Contributor

No description provided.

@Zimmi48 Zimmi48 added the kind: infrastructure CI, build tools, development tools. label Sep 20, 2017
@Zimmi48
Copy link
Member
Zimmi48 commented Sep 20, 2017

What about giving a more generic name to this variable like just BRANCH, setting it to TRAVIS_BRANCH in case we are on Travis, and adapting the code in dev/ci/user-overlays to this change? We could even have a fallback in case we are neither on Travis nor on GitLab CI and use git branch | grep \* | cut -d ' ' -f2...

@SkySkimmer
Copy link
Contributor Author

If we want to be robust we should just not merge user overlays into master and make them unconditional.

@Zimmi48
Copy link
Member
Zimmi48 commented Sep 20, 2017

Yeah, well historically @ejgallego wanted us to merge user overlays in master to keep some historical record but @maximedenes disagreed and merged PRs after dropping commits adding user-overlays (and when we first submit a PR with a backward compatible fix and it gets merged before the PR, the author is generally the one who drops the user overlay).
I guess the main advantage of having this logic is that even if we forget to remove the user overlay, it won't affect our testing once merged. The main disadvantage is that people seem to think that it is OK to instead change the basic overlay in ci-basic-overlay.sh, so that we now get a polluted file with lots of development being tracked elsewhere than on the official repository.

@ejgallego
Copy link
Member

Yup, a polluted ci-basic-overlay should be a blocker for merging.

@Zimmi48
Copy link
Member
Zimmi48 commented Sep 20, 2017

Unfortunately, it currently isn't. See my rant at #914 (comment).

@maximedenes
Copy link
Member

@SkySkimmer Should I merge this?

@SkySkimmer
Copy link
Contributor Author

Please do merge.

@coqbot coqbot merged commit cb12138 into rocq-prover:master Sep 22, 2017
coqbot pushed a commit that referenced this pull request Sep 22, 2017
@maximedenes
Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will wor…
63b3b3f 
…k as expected.
@Zimmi48 Zimmi48 added this to the 8.8 milestone Sep 22, 2017
@SkySkimmer SkySkimmer deleted the gitlab-overlay-branch branch October 4, 2017 09:48
@Zimmi48 Zimmi48 modified the milestones: 8.8, 8.7.2 Jan 8, 2018
Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Jan 8, 2018
@Zimmi48
Backport PR rocq-prover#1065: In gitlab set TRAVIS_BRANCH so user ove…
3058fa9 
…rlays will work as expected.
Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Jan 8, 2018
@Zimmi48
Backport PR rocq-prover#1065: In gitlab set TRAVIS_BRANCH so user ove…
e885266 
…rlays will work as expected.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: infrastructure CI, build tools, development tools.
Projects
None yet
Milestone
8.7.2
Development

Successfully merging this pull request may close these issues.
5 participants
@SkySkimmer @Zimmi48 @ejgallego @maximedenes @coqbot
0