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.

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 pre-commit maintenance #1905

Merged
merged 18 commits into from
Mar 23, 2023
Merged

CI pre-commit maintenance #1905

merged 18 commits into from
Mar 23, 2023

Conversation

jonaprieto
Copy link
Collaborator

@jonaprieto jonaprieto commented Mar 21, 2023 •
edited
Loading

This PR goes after:

Included in this PR:

  • Add Clang formatting (v.15) as part of the pre-commits.
  • Add new pre-commits:
    • forbid binary files
    • check toml files for mdbook
    • detect-private-key
    • format-juvix-examples: check all the Juvix programs in the examples folder type-check for local runs.
  • Remove .pre-commit-hooks and add ormolu for local pre-commit runs instead.

@jonaprieto jonaprieto self-assigned this Mar 21, 2023
@jonaprieto jonaprieto added enhancement New feature or request CI labels Mar 21, 2023
@jonaprieto jonaprieto added this to the 0.3.1 milestone Mar 21, 2023
@jonaprieto jonaprieto requested a review from paulcadman March 21, 2023 13:40
@jonaprieto jonaprieto mentioned this pull request Mar 21, 2023
Merged
@jonaprieto jonaprieto marked this pull request as ready for review March 22, 2023 15:47
paulcadman
paulcadman approved these changes Mar 23, 2023
View reviewed changes
Copy link
Collaborator

@paulcadman paulcadman left a comment

Choose a reason for hiding this comment

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

🚀

@paulcadman paulcadman merged commit 839093c into main Mar 23, 2023
@paulcadman paulcadman deleted the pre-commit-fixes branch March 23, 2023 08:57
jonaprieto added a commit that referenced this pull request Mar 23, 2023
@jonaprieto
Update GitHub pages deployment using deploy-pages action (#1910)
dbe9ff6 
This PR changes two things:

- Deploy the documentation website using the (official) deploy action:
  - https://github.com/actions/deploy-pages
- Check the documentation generation for all the PRs. 

- PR on top of:
  - #1905 
  - #1908   

After merging this PR, we could delete the github-pages branch.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@paulcadman paulcadman paulcadman approved these changes

Assignees

@jonaprieto jonaprieto

Labels
CI enhancement New feature or request
Projects
None yet
Milestone
0.3.1
Development

Successfully merging this pull request may close these issues.
2 participants
@jonaprieto @paulcadman