# 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"