-
Notifications
You must be signed in to change notification settings - Fork 33
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
Deploy several documentations #1169
Conversation
c3da7ea
to
70b6d62
Compare
.github/workflows/build_doc.yml
Outdated
uses: JamesIves/github-pages-deploy-action@v4 | ||
with: | ||
deploy_key: ${{ secrets.ACTIONS_DEPLOY_KEY }} | ||
publish_dir: build_doc | ||
destination_dir: dev | ||
enable_jekyll: true | ||
folder: build_doc | ||
target-folder: dev |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We used to have:
# Deploy files contain in _build directory on gh-pages branch
- name: deploy-doc
uses: JamesIves/[email protected]
with:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
BRANCH: gh-pages
FOLDER: _build
CLEAN: false
does that no longer work?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also possibly you need to deploy from a branch in the repository (not from a fork)?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You can try directly on your fork if you enable GH actions on your fork (although you may need to enable GH pages as well, not sure)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Both does not work so it seems we cannot deploy from a PR I guess. I will try on my fork.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It works on my fork... aahhhhhhhhhhhhhhhh
3cf1c90
to
05fc660
Compare
This PR adds the ability to deploy several documentations of Alt-Ergo. Basically, we push the documentation of the dev version in `/dev` on gh-pages if we push on `next`.
I gave up. |
This PR adds the ability to deploy several documentations of Alt-Ergo. The new documentation workflows work as follows:
build_doc
builds both sphinx and odoc documentations and merges them in a single artifact. This workflow is trigger after pushing on PR;next
, the newgh-pages
workflow retrieves the previous artifact and deploy it in the directory/dev
of thegh-pages
branch;doc
of our makefile and update theindex.mld
file ofgh-pages
.This PR fixes #693
I also removed the support for
gtk-lang
of the native input because we removed the GUI.