From ab3b0de5902082f7e692901979aa8330394c2f26 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Nov 2016 12:58:02 +0100
Subject: Fixing printing of "Set Warnings Append".

---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 (
-- 
cgit v1.2.3