diff -r 821ce370b7fc -r eec610972763 etc/options
--- a/etc/options	Sat Jul 27 22:16:04 2013 +0200
+++ b/etc/options	Sat Jul 27 22:20:25 2013 +0200
@@ -6,7 +6,7 @@
   -- "generate theory browser information"
 
 option document : string = ""
-  -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
+  -- "build document in given format: pdf, dvi, false"
 option document_output : string = ""
   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
 option document_variants : string = "document"