diff options
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9533833212..5d6d36d569 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1131,7 +1131,7 @@ module Make | VernacSetAppendOption (na,v) -> return ( hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ - spc() ++ keyword "Append" ++ spc() ++ str v) + spc() ++ keyword "Append" ++ spc() ++ qs v) ) | VernacAddOption (na,l) -> return ( |