aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/vernac_classifier.ml')
-rw-r--r--stm/vernac_classifier.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index fa7acd00a..dc5be08a3 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -181,7 +181,7 @@ let rec classify_vernac e =
| VernacReserve _
| VernacGeneralizable _
| VernacSetOpacity _ | VernacSetStrategy _
- | VernacUnsetOption _ | VernacSetOption _
+ | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _
| VernacAddOption _ | VernacRemoveOption _
| VernacMemOption _ | VernacPrintOption _
| VernacGlobalCheck _