8000 [docker] [ci] Have docker CI use the jscoq branch in pull request builds by ejgallego · Pull Request #321 · jscoq/jscoq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

[docker] [ci] Have docker CI use the jscoq branch in pull request builds #321

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

Merged
merged 1 commit into from
Sep 16, 2024

Conversation

ejgallego
Copy link
Member
@ejgallego ejgallego commented Jan 31, 2023

No description provided.

@ejgallego
Copy link
Member Author

Oh, actually the docker file was not pulling from this PR, trying to fix this.

@ejgallego
Copy link
Member Author

There are still some mess with how to set the proper entry point, hope to fix that later.

@ejgallego ejgallego force-pushed the fix_docker branch 2 times, most recently from 6909ceb to 058e533 Compare February 1, 2023 22:30
@corwin-of-amber
Copy link
Member

Hmm we forgot about this PR. Is it obsolete at this point?

@ejgallego
Copy link
Member Author

Actually I think still some parts of it are needed, let me have a look.

@ejgallego ejgallego modified the milestones: 0.16.1, 0.17.0 Jul 24, 2023
@ejgallego ejgallego changed the title [build] Fix Docker and make dist [docker] [ci] Have docker CI use the jscoq branch in pull request builds Jul 25, 2023
@ejgallego ejgallego modified the milestones: 0.17.0, 0.17.0+lsp Aug 9, 2023
@ejgallego ejgallego modified the milestones: 0.17.0+lsp, 2.0 Sep 16, 2024
@ejgallego ejgallego changed the base branch from v8.16 to v8.20+lsp September 16, 2024 15:28
@ejgallego ejgallego merged commit cd8230e into v8.20+lsp Sep 16, 2024
2 of 3 checks passed
@ejgallego ejgallego deleted the fix_docker branch September 16, 2024 16:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants
0