# HG changeset patch
# User wenzelm
# Date 1509390564 -3600
# Node ID eefbb2300669a89ebd92960c30a46c1add448256
# Parent  3d8fd98c7c8614117c531cc5f5624627f21c7931
tuned;

diff -r 3d8fd98c7c86 -r eefbb2300669 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Mon Oct 30 20:04:10 2017 +0100
+++ b/src/Doc/System/Environment.thy	Mon Oct 30 20:09:24 2017 +0100
@@ -255,8 +255,8 @@
   "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
   to do that programmatically via the \<^verbatim>\<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>}
+  directory). For example:
+  @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
 
   This is tolerant wrt.\ missing component directories, but might produce a
   warning.