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

Hotfix/gh pages #2035

Merged
merged 7 commits into from
Aug 24, 2023
Merged

Hotfix/gh pages #2035

merged 7 commits into from
Aug 24, 2023

Conversation

F-WRunTime
Copy link
Member

Think I figured out what's wrong with the gh-pages build. This should fix it. I have a temp repository built on my local box I can try to push the gh-pages with if we'd like to try it first before releasing this into CI.

…submodules, k-web-theme isn't setup properly adding explicit submodule init and update
@F-WRunTime F-WRunTime self-assigned this Aug 24, 2023
@F-WRunTime
Copy link
Member Author

F-WRunTime commented Aug 24, 2023

To answer your other question, the k-web-theme submodule was still being used as part of the npm build definition in web/package.json

@ehildenb ehildenb merged commit ba06470 into master Aug 24, 2023
12 checks passed
@ehildenb ehildenb deleted the hotfix/gh-pages branch August 24, 2023 21:54
iFrostizz pushed a commit that referenced this pull request Aug 28, 2023
* Do not remove gitmodules

* gh-pages needs the .gitmodules info to checkout appropriate web/ and submodules, k-web-theme isn't setup properly adding explicit submodule init and update

* Set Version: 1.0.276

* Remove manual submodule checkout

* Set Version: 1.0.277

* Set Version: 1.0.278

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
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