# HG changeset patch
# User wenzelm
# Date 1504200582 -7200
# Node ID 7d4da1c62de709610012ae22ae4238ef81e34869
# Parent  191048506504268d619b56e9578b7a4bacb5c9df
tuned;

diff -r 191048506504 -r 7d4da1c62de7 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>