--- a/src/Doc/System/Sessions.thy Sun Oct 16 20:19:10 2016 +0200
+++ b/src/Doc/System/Sessions.thy Sun Oct 16 22:43:51 2016 +0200
@@ -257,6 +257,7 @@
Options are:
-D DIR include session directory and select its sessions
+ -N cyclic shuffling of NUMA CPU nodes (performance tuning)
-R operate on requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
@@ -349,6 +350,10 @@
worker threads, cf.\ system option @{system_option_ref threads}.
\<^medskip>
+ Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help
+ performance tuning on Linux servers with separate CPU/memory modules.
+
+ \<^medskip>
Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting