# HG changeset patch
# User wenzelm
# Date 1590582771 -7200
# Node ID 0da5fb75088a88fabe0c47d5b01b2b266c474820
# Parent  1529336eaedc7a8e2d5956fd8b80c62c1d38a033
more antiquotations;

diff -r 1529336eaedc -r 0da5fb75088a src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Wed May 27 14:27:22 2020 +0200
+++ b/src/Doc/System/Environment.thy	Wed May 27 14:32:51 2020 +0200
@@ -249,7 +249,7 @@
   After initializing all of its sub-components recursively, @{setting
   ISABELLE_HOME_USER} is included in the same manner (if that directory
   exists). This allows to install private components via \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>, although it is often more convenient
-  to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
+  to do that programmatically via the \<^bash_function>\<open>init_component\<close> shell function in the
   \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
   directory). For example:
   @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}