diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-21 12:58:02 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-12-02 15:30:37 +0100 |
| commit | ab3b0de5902082f7e692901979aa8330394c2f26 (patch) | |
| tree | e0beb1cb5c83fc7ae2257ce1a4b23bac01421564 /printing | |
| parent | edb7a97487cb5e38bb284472eacfd1b58fa97f84 (diff) | |
Fixing printing of "Set Warnings Append".
Diffstat (limited to 'printing')
| -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 953383321..5d6d36d56 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 ( |