equal
deleted
inserted
replaced
134 is available: |
134 is available: |
135 |
135 |
136 @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>} |
136 @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>} |
137 |
137 |
138 \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name |
138 \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name |
139 of the @{executable isabelle} executable. Thus other tools and scripts need |
139 of the @{executable isabelle} executable. |
140 not assume that the \<^dir>\<open>$ISABELLE_HOME/bin\<close> directory is on the current |
|
141 search path of the shell. |
|
142 |
140 |
143 \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this |
141 \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this |
144 Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017\<close>''. |
142 Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017\<close>''. |
145 |
143 |
146 \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def |
144 \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def |