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

Remove pauses in configure script #1305

Merged
merged 1 commit into from
Sep 23, 2024

Conversation

digama0
Copy link
Contributor

@digama0 digama0 commented Sep 21, 2024

When determining the properties of dependencies, it would pause for 1 second after each one, making it look like more work than it actually is and also slowing down the tool. I left the 3 second countdown after all settings are confirmed, although 3 seconds is a bit short for a human to respond to the information.

@mn200
Copy link
Member

mn200 commented Sep 23, 2024

Fair enough!

@mn200 mn200 merged commit c7ca762 into HOL-Theorem-Prover:develop Sep 23, 2024
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants