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

Add a config option to control tactics' auto's gas #1355

Closed
isovector opened this issue Feb 12, 2021 · 4 comments · Fixed by #1771
Closed

Add a config option to control tactics' auto's gas #1355

isovector opened this issue Feb 12, 2021 · 4 comments · Fixed by #1771
Labels

Comments

@isovector
Copy link
Collaborator

It would allow us to solve things like #562

@isovector
Copy link
Collaborator Author

Additionally, maybe automatically increase the gas if a hole fill doesn't produce any results.

@jneira jneira added the type: enhancement New feature or request label Feb 12, 2021
@jneira
Copy link
Member

jneira commented Feb 12, 2021

Only want to note that now plugins has its own namespace in our config: #691

@isovector
Copy link
Collaborator Author

Thanks for the info, @jneira . Do these options show up in editors' configuration settings?

@jneira
Copy link
Member

jneira commented Feb 12, 2021

I am afraid they still not are, there is an issue about haskell/vscode-haskell#336
You can do it manually though: #1342 (comment)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants