8000 Follow hlint suggestion: use gets by philderbeast · Pull Request #7400 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
8000

Follow hlint suggestion: use gets #7400

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

Merged
merged 2 commits into from
Jul 30, 2024
Merged

Conversation

philderbeast
Copy link
Contributor

Sorry @andreasabel. Yesterday I ran the following command to install hlint-3.8 but somehow ended up with a local build that was not the published version (should have also checked the path to the exe was ~/.cabal/bin/hlint) so there's an extra commit (that resets the "warnings triggered" properly) included with this pull request. The "Empty single-line comment" should have been a give away as that is part of ndmitchell/hlint#1459 and not yet included in hlint. I was not being careful enough.

$ cabal install hlint-3.8 --overwrite-policy=always --ignore-project

The second commit follows the hlint suggestion to use gets.

@andreasabel andreasabel added the dev: hlint About using 'hlint' for code style (not in changelog) label Jul 30, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Jul 30, 2024
@andreasabel andreasabel merged commit a96930b into agda:master Jul 30, 2024
27 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
dev: hlint About using 'hlint' for code style (not in changelog)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants
0