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

Deploy several documentations #1169

Closed
wants to merge 4 commits into from

Conversation

Halbaroth
Copy link
Collaborator

@Halbaroth Halbaroth commented Jul 17, 2024

This PR adds the ability to deploy several documentations of Alt-Ergo. The new documentation workflows work as follows:

  • the workflow build_doc builds both sphinx and odoc documentations and merges them in a single artifact. This workflow is trigger after pushing on PR;
  • while pushing on next, the new gh-pages workflow retrieves the previous artifact and deploy it in the directory /dev of the gh-pages branch;
  • if we want to add a new release documentation, we have to do by hand using the target doc of our makefile and update the index.mld file of gh-pages.

This PR fixes #693

I also removed the support for gtk-lang of the native input because we removed the GUI.

Comment on lines 56 to 59
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
Copy link
Collaborator

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/github-pages-deploy-action@3.6.2
        with:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          BRANCH: gh-pages
          FOLDER: _build
          CLEAN: false

does that no longer work?

Copy link
Collaborator

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)?

Copy link
Collaborator

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)

Copy link
Collaborator Author

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.

Copy link
Collaborator Author

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

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`.
@Halbaroth
Copy link
Collaborator Author

I gave up.

@Halbaroth Halbaroth closed this Jul 22, 2024
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.

Make sure that the documentation on the website is that of the last release
2 participants