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

Accommodate rapid website development on the website branch #287

Merged
merged 7 commits into from
Oct 11, 2022

Conversation

rickie
Copy link
Member

@rickie rickie commented Oct 10, 2022

No description provided.

@rickie rickie added the chore A task not related to code (build, formatting, process, ...) label Oct 10, 2022
@rickie rickie added this to the 0.4.0 milestone Oct 10, 2022
@@ -2,7 +2,7 @@ name: Update `error-prone.picnic.tech` website content
on:
pull_request:
push:
branches: [ master ]
branches: [ master, develop ]
Copy link
Member

Choose a reason for hiding this comment

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

Why do we need develop? That branch didn't exist before.

Copy link
Member

Choose a reason for hiding this comment

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

Below we're mentioning website, so perhaps it should be s/develop/website/?

Copy link
Member Author

Choose a reason for hiding this comment

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

You are right, not sure why I typed develop 😅. Pushed the tweak.

Copy link
Member

Choose a reason for hiding this comment

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

I think we can omit this, as long as you open a draft PR. Would that work? Or is there a strong preference to keep using a branch?

Copy link
Member Author

Choose a reason for hiding this comment

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

For now it would be nice to be able to quickly push something to that branch, such that it'll build. Making draft PRs is a bit more cumbersome. We can revert this after we have everything stable and merged the way we want it.

For now it'll allow us to iterate quickly.

Copy link
Member

Choose a reason for hiding this comment

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

In that case, we don't even need to merge this PR. Just push this change on the website branch, and it'll work :)

@@ -35,7 +35,7 @@ jobs:
with:
path: ./website/_site
deploy:
if: github.ref == 'refs/heads/master'
if: github.ref == 'refs/heads/master' || github.ref == 'refs/heads/website'
Copy link
Member

Choose a reason for hiding this comment

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

Also requires a change in our environment settings to allow this branch to deploy.

@Stephan202
Copy link
Member

I would have expected this PR to be just s/master/website/, such that merges to the default branch don't revert the work on website :)

Assuming that's the intention, a suggested commit message could be:

Deploy the website from the `website` branch (#287)

@rickie
Copy link
Member Author

rickie commented Oct 10, 2022

I understood something slightly different. Anyway, updated the PR.

@@ -2,7 +2,7 @@ name: Update `error-prone.picnic.tech` website content
on:
pull_request:
push:
branches: [ master, website ]
branches: [ website ]
Copy link
Member

Choose a reason for hiding this comment

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

IIUC, if we wish to run the build job still on master, it should be added to the branches here. This will not overwrite the website as the deploy job does not run on master.

Suggested change
branches: [ website ]
branches: [ master, website ]

Copy link
Member Author

Choose a reason for hiding this comment

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

Ah that would be nice actually, warns us whenever there is an error there. As long as it doesn't override the website for every new merge :).

Copy link
Member

@Badbond Badbond left a comment

Choose a reason for hiding this comment

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

Based on my understanding, I assume this'll work as intended. 👍

@Stephan202
Copy link
Member

@rickie will add one more commit "soon" 👀

Copy link
Member

@Stephan202 Stephan202 left a comment

Choose a reason for hiding this comment

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

Added a small commit. Arguably we should also have an XXX comment to drop the website references later, but let's roll.

Suggested commit message:

Accommodate rapid website development on the `website` branch (#287)

By (a) deploying from that branch and (b) temporarily disabling external link
checking.

@rickie rickie changed the title Allow error-prone.picnic.tech deployments from the website branch Accommodate rapid website development on the website branch Oct 11, 2022
@rickie rickie merged commit 3f1399c into master Oct 11, 2022
@rickie rickie deleted the rossendrijver/deploy-on-website-push branch October 11, 2022 12:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
chore A task not related to code (build, formatting, process, ...)
Development

Successfully merging this pull request may close these issues.

4 participants