Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Changing moreLeanArgs does not trigger recompilation #50

Closed
Kha opened this issue Jan 25, 2022 · 0 comments
Closed

Changing moreLeanArgs does not trigger recompilation #50

Kha opened this issue Jan 25, 2022 · 0 comments
Labels
bug Something isn't working enhancement New feature or request

Comments

@Kha
Copy link
Member

Kha commented Jan 25, 2022

No description provided.

@tydeu tydeu added bug Something isn't working enhancement New feature or request labels Jan 25, 2022
@tydeu tydeu closed this as completed in 463c4f0 May 19, 2022
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug Something isn't working enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants