aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/flags.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-09-28 16:08:40 +0200
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-09-28 16:32:52 +0200
commitdaae678047ee2a1c53d4dc423976f77e40ba753f (patch)
treef97544bfe1d3b94d833f5ae4c8620ca6024b9309 /lib/flags.ml
parent3d3d70508e0f33ca1b9c6e04f62b0b3287e97f26 (diff)
FIX: a bug in the pattern matching
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index df00eba7b..40b7a29d2 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -122,7 +122,7 @@ let version_strictly_greater v = match !compat_version, v with
| _ , V8_4 -> false
| V8_4 , _ -> true
| _ , V8_3 -> false
-| v8_3 , _ -> true
+| V8_3 , _ -> true
| V8_2 , V8_2 -> false