REDUCE configuration updates
- Add buttons to move the current REDUCE command up or down the list cyclically.
- Save and restore the order of REDUCE commands.
- When duplicating a REDUCE command, add it to the bottom of the list rather than below the current command.
- Expand ~/ or ~\ to the user's home directory (on all platforms).
- Rename the preference key reduceVersions to reduceCommands, with backward compatibility code to be deleted later.
- Display directory or file errors as warnings and allow the user to ignore them.
- Add a button to reset the selected command to its default configuration.
- Add checkboxes for running REDUCE using the default shell and not checking the command pathname. Only append Pathname to the Command label when appropriate.
- The Command Root Directory chooser and file choosers use current Command Root Directory field value if defined, else the REDUCE Root Directory field value if defined, else the default REDUCE Root Directory as initial directory.
- The file choosers replace the root segment of the chosen path by $REDUCE if possible.
- Change all default configurations to use the default system shell, which is much simpler and more likely to be robust against possible changes to REDUCE.
- Change the default Linux configuration to use the search path and not check the command pathname, making it easier to transition from the previous defaults.
- Substantially revise the Configure REDUCE... section of the User Guide.
If you have saved a non-default REDUCE configuration that you want to keep then I recommend you install this release and open the REDUCE Configuration dialogue. Select each of the default REDUCE commands in turn and click on the Reset Selected Command button. Then click on the Save button. This will read from the old preference key and write to the new one, and also update the default commands.
If you have ever saved the default REDUCE configuration then I recommend you install this release and open the REDUCE Configuration dialogue. Click on the Reset All Defaults button. Then click on the Save button. This will update the saved configuration to the new defaults.