# HG changeset patch
# User wenzelm
# Date 1343499635 -7200
# Node ID f9732774ffc7c54c2e22313d24150dd639c4d1a6
# Parent  500c6eb6c6dcc1608ad31f4391ab2c6bd06b64fd
no apparent need for single-threaded execution;

diff -r 500c6eb6c6dc -r f9732774ffc7 doc-src/ROOT
--- a/doc-src/ROOT	Sat Jul 28 20:18:15 2012 +0200
+++ b/doc-src/ROOT	Sat Jul 28 20:20:35 2012 +0200
@@ -73,8 +73,7 @@
 
 session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
   options [browser_info = false, document = false,
-    document_dump = document, document_dump_mode = "tex",
-    threads = 1]  (* FIXME *)
+    document_dump = document, document_dump_mode = "tex"]
   theories [document_dump = ""]
     "~~/src/HOL/Library/LaTeXsugar"
     "~~/src/HOL/Library/OptionalSugar"