equal
deleted
inserted
replaced
253 ISABELLE_HOME_USER} is included in the same manner (if that directory |
253 ISABELLE_HOME_USER} is included in the same manner (if that directory |
254 exists). This allows to install private components via @{path |
254 exists). This allows to install private components via @{path |
255 "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient |
255 "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient |
256 to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the |
256 to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the |
257 \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component |
257 \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component |
258 directory). For example: @{verbatim [display] \<open>init_component |
258 directory). For example: |
259 "$HOME/screwdriver-2.0"\<close>} |
259 @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>} |
260 |
260 |
261 This is tolerant wrt.\ missing component directories, but might produce a |
261 This is tolerant wrt.\ missing component directories, but might produce a |
262 warning. |
262 warning. |
263 |
263 |
264 \<^medskip> |
264 \<^medskip> |