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

[ci] Manual doc build uses deploy-doc, remove doc build from pr ci. #1089

Merged

dlyr merged 1 commit into STORM-IRIT:release-candidate from dlyr:manual-doc-build

Oct 11, 2024

Contributor

dlyr commented Oct 11, 2024

Remove duplicated code in CI (I had forgotten we have a manual doc build action).


          [ci] Manual doc build uses deploy-doc, remove doc build from pr ci.

e6109c6

dlyr merged commit ff4df84 into STORM-IRIT:release-candidate

12 checks passed

Contributor Author

dlyr commented Oct 11, 2024 •

edited

Loading

Will work when merged to master.
Tested by switching default branch to release-candidate and triggererd manually : https://github.com/STORM-IRIT/Radium-Engine/actions/runs/11297031930

dlyr deleted the manual-doc-build branch

October 11, 2024 18:00

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet