diff options
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index b9d8ac42b1..f448dd4ed1 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -673,7 +673,7 @@ let _ = let dot = if fn.[0]='/' then "." else "" in command ("mv "^dir^"/"^dot^"*.html "^fn^".xml "); command ("rm "^fn^".v"); - print_string("\nWriting on file \"" ^ fn ^ ".xml\" was succesful\n")) + print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n")) ofn) ;; |