This repository has been archived by the owner on Dec 2, 2024. It is now read-only.

Remove accidental change #506

Merged

sjoerdvisscher merged 1 commit into main from remove-ghc-options

Jun 9, 2022

Contributor

sjoerdvisscher commented Jun 9, 2022

Pre-submit checklist:

Branch
- Tests are provided (if possible)
- Commit sequence broadly makes sense
- Key commits have useful messages
- Formatting, PNG optimization, etc. are updated
PR
- Self-reviewed the diff
- Useful pull request description
- Reviewer requested


          Remove acidental change

711c630

sjoerdvisscher changed the title ~~Remove acidental change~~ Remove accidental change

sjoerdvisscher merged commit ed54a2b into main

sjoerdvisscher deleted the remove-ghc-options branch

June 9, 2022 14:17

koslambrou pushed a commit that referenced this pull request


          Remove acidental change (#506)

0db7dd9

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

Labels

None yet