# 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>\<open>-d\<close> specifies an laternative document output directory. The default
+  Option \<^verbatim>\<open>-d\<close> specifies an alternative document output directory. The default
   is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
   will appear in the parent of this directory.