From d6c45c99a9fd0dae4932f375ac663c368b1bdaf3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 2 Nov 2019 22:06:07 +0100
Subject: Run update-compat script with --release option.

This should ideally have been done before the 8.11 branching.
---
 vernac/g_vernac.mlg | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index b4c0a33585..4243d0c911 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -65,8 +65,7 @@ let parse_compat_version = let open Flags in function
   | "8.11" -> Current
   | "8.10" -> V8_10
   | "8.9" -> V8_9
-  | "8.8" -> V8_8
-  | ("8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+  | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
     CErrors.user_err ~hdr:"get_compat_version"
       Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
   | s ->
-- 
cgit v1.2.3