Skip to content
This repository was archived by the owner on Dec 2, 2024. It is now read-only.

Remove accidental change#506

Merged
sjoerdvisscher merged 1 commit intomainfrom
remove-ghc-options
Jun 9, 2022
Merged

Remove accidental change#506
sjoerdvisscher merged 1 commit intomainfrom
remove-ghc-options

Conversation

@sjoerdvisscher
Copy link
Contributor

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

@sjoerdvisscher sjoerdvisscher changed the title Remove acidental change Remove accidental change Jun 9, 2022
@sjoerdvisscher sjoerdvisscher merged commit ed54a2b into main Jun 9, 2022
@sjoerdvisscher sjoerdvisscher deleted the remove-ghc-options branch June 9, 2022 14:17
koslambrou pushed a commit that referenced this pull request Jun 22, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant