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

improve hints on splash; fix quick options saving #791

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

hendriktews
Copy link
Collaborator

  • add menu entry to disable splash screen to quick options
  • add info to the splash screen on how to leave and disable the splash screen
  • add Proof-General menu to splash screen, such that the hints on the splash screen make sense
  • fix saving of quick options for several options
  • the CHANGES entry also describes commit ea0f007
  • adapt manual

- add menu entry to disable splash screen to quick options
- add info to the splash screen on how to leave and disable the splash
  screen
- add Proof-General menu to splash screen, such that the hints on the
  splash screen make sense
- fix saving of quick options for several options
- the CHANGES entry also describes commit ea0f007
- adapt manual
@hendriktews
Copy link
Collaborator Author

@Matafou @erikmd : With the information about how to disable the splash screen present on the splash screen, I think we can and also should increase the splash screen time again, maybe 3 or 4 seconds. With 1 second, it is impossible to see that there is information about how to disable it. What do you think?
Having said that, I don't care too much and we can also leave as is -- I have disabled the splash screen for decades already.

@erikmd
Copy link
Member

erikmd commented Oct 4, 2024

With the information about how to disable the splash screen present on the splash screen, I think we can and also should increase the splash screen time again, maybe 3 or 4 seconds. With 1 second, it is impossible to see that there is information about how to disable it. What do you think?

IMHO, I would not come back to a 3--4 seconds delay:

I would just disable the splash feature by default, or ideally (to be less "aggressive") modify the splash feature so that the *Proof General Welcome* buffer is still created, but in the background (i.e. similarly to calling M-x bury-buffer RET).
Both approaches would be an acceptable workaround to me.
WDYT?

@monnier
Copy link
Contributor

monnier commented Oct 4, 2024 via email

@Matafou
Copy link
Contributor

Matafou commented Oct 4, 2024

Agreed. A "about" command would be better.

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.

4 participants