99 exists) is run in the same way as the site default settings. Note |
99 exists) is run in the same way as the site default settings. Note |
100 that the variable @{setting ISABELLE_HOME_USER} has already been set |
100 that the variable @{setting ISABELLE_HOME_USER} has already been set |
101 before --- usually to something like @{verbatim |
101 before --- usually to something like @{verbatim |
102 "$USER_HOME/.isabelle/IsabelleXXXX"}. |
102 "$USER_HOME/.isabelle/IsabelleXXXX"}. |
103 |
103 |
104 Thus individual users may override the site-wide defaults. See also |
104 Thus individual users may override the site-wide defaults. |
105 file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the |
105 Typically, a user settings file contains only a few lines, with some |
106 distribution. Typically, a user settings file would contain only a |
106 assignments that are actually changed. Never copy the central |
107 few lines, just the assigments that are really changed. One should |
107 @{file "$ISABELLE_HOME/etc/settings"} file! |
108 definitely \emph{not} start with a full copy the basic @{file |
|
109 "$ISABELLE_HOME/etc/settings"}. This could cause very annoying |
|
110 maintainance problems later, when the Isabelle installation is |
|
111 updated or changed otherwise. |
|
112 |
108 |
113 \end{enumerate} |
109 \end{enumerate} |
114 |
110 |
115 Since settings files are regular GNU @{executable_def bash} scripts, |
111 Since settings files are regular GNU @{executable_def bash} scripts, |
116 one may use complex shell commands, such as @{verbatim "if"} or |
112 one may use complex shell commands, such as @{verbatim "if"} or |