Naso (Jun 07 2023 at 03:48): Naso (Jun 07 2023 at 03:48):Hello, how can I reset the jedit window settings on Mac? Thank you
Naso (Jun 24 2023 at 12:03):Can no one help me? I accidentally closed the "Output" tab and cannot get it to come back.
Mathias Fleury (Jun 24 2023 at 12:30):Plugins > Isabelle > Output panel
I don't remember if you have to dock to the bottom afterwards.
Naso (Jun 24 2023 at 13:34):Mathias Fleury said:
I don't remember if you have to dock to the bottom afterwards.
Thank you Mathias :) This restored the output panel but now it is floating. Do you know how I can dock it?
Mathias Fleury (Jun 24 2023 at 13:35):somewhere right-click > dock at
Mathias Fleury (Jun 24 2023 at 13:36):the small triangle arrow, top left
Naso (Jun 24 2023 at 13:38):right-clicking anywhere in the floating output window doesn't appear to do anything
Naso (Jun 24 2023 at 13:38):(on macOS)
Naso (Jun 24 2023 at 13:39):ohh...
image.png
Naso (Jun 24 2023 at 13:40):there is an extremely tiny black triangle in the top left, above a grey background
Naso (Jun 24 2023 at 13:40):and clicking on it works!
Naso (Jun 24 2023 at 13:40):thank you :)
Last updated: Apr 28 2024 at 04:17 UTC