user_guide:shell

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revisionBoth sides next revision
user_guide:shell [2021/01/12 15:53] – [Switching between applications] gawrilowuser_guide:shell [2021/01/12 15:54] – [History and replaying] gawrilow
Line 45: Line 45:
   :: appends the commands stored in the given file to the history, rewinds back to the first of them, and turns on the replay mode.  This command is especially useful for making live demos with polymake, as you can prepare and test your input in advance and don't have to waste your time for typing during the presentation.   :: appends the commands stored in the given file to the history, rewinds back to the first of them, and turns on the replay mode.  This command is especially useful for making live demos with polymake, as you can prepare and test your input in advance and don't have to waste your time for typing during the presentation.
      
-Finally, let's mention two [[howto:shell_custom|custom variables]] related to the history handling.+Finally, let's mention two [[user_guide:howto:shell_custom|custom variables]] related to the history handling.
  
   ? ''$history_size''   ? ''$history_size''
  • user_guide/shell.txt
  • Last modified: 2021/01/12 15:55
  • by gawrilow