Commits on Oct 2, 2024

1. improve hints on splash; fix quick options saving …

   - 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 committed Oct 2, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 739ebaf
   • Browse repository at this point

   Copy the full SHA

   739ebaf View commit details

   Browse the repository at this point in the history