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

Add website update #226

Merged
merged 1 commit into from
Apr 13, 2022
Merged

Add website update #226

merged 1 commit into from
Apr 13, 2022

Conversation

fsimonis
Copy link
Member

@fsimonis fsimonis commented Mar 14, 2022

This PR adds a workflow which triggers the website repo to update its submodules in case the documentation changes on develop.

Can we test this PR without merging it directly?

@fsimonis fsimonis requested a review from MakisH March 14, 2022 14:58
@fsimonis fsimonis self-assigned this Mar 14, 2022
Copy link
Member

@MakisH MakisH left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks to me like a good addition and the code looks reasonable. I am not sure how to test it, but I also don't think we need to test this before merging: it should only trigger a workflow that we are always fine if it is triggered.

The docs/** pattern is enough.

@MakisH MakisH merged commit bf38c42 into develop Apr 13, 2022
@MakisH MakisH deleted the add-website-update branch April 13, 2022 06:58
@MakisH MakisH added this to the v1.2.0 milestone Sep 19, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants