# HG changeset patch # User haftmann # Date 1515319954 -3600 # Node ID 63d7aca15f6b1ae41f91bee3f9f75036dbfc0273 # Parent f061129d891b4938911dcd5a74cf928a2d70ee38 spelling diff -r f061129d891b -r 63d7aca15f6b src/Doc/System/Presentation.thy --- a/src/Doc/System/Presentation.thy Sat Jan 06 22:55:52 2018 +0100 +++ b/src/Doc/System/Presentation.thy Sun Jan 07 11:12:34 2018 +0100 @@ -167,7 +167,7 @@ run. \<^medskip> - Option \<^verbatim>\-d\ specifies an laternative document output directory. The default + Option \<^verbatim>\-d\ specifies an alternative document output directory. The default is \<^verbatim>\output/document\ (derived from the document name). Note that the result will appear in the parent of this directory.