tuned;
authorwenzelm
Thu, 31 Aug 2017 19:29:42 +0200
changeset 66576 7d4da1c62de7
parent 66575 191048506504
child 66577 6e35cf3ce869
tuned;
src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Thu Aug 31 19:06:14 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Thu Aug 31 19:29:42 2017 +0200
@@ -318,7 +318,7 @@
   Any session root directory may refer recursively to further directories of
   the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This
   helps to organize large collections of session specifications, or to make
-  \<^verbatim>\<open>-d\<close> command line options persistent (say within
+  \<^verbatim>\<open>-d\<close> command line options persistent (e.g.\ in
   \<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
 
   \<^medskip>