From fb4122afb90f3535720f13472b74dcf96884f4de Mon Sep 17 00:00:00 2001 From: Jeremie Dimino Date: Wed, 1 Mar 2017 13:31:08 +0000 Subject: [PATCH] Fix bootstrap with 4.02 --- bootstrap.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bootstrap.ml b/bootstrap.ml index 51b142c3..bcc4307f 100644 --- a/bootstrap.ml +++ b/bootstrap.ml @@ -265,7 +265,7 @@ module Jbuilder_re = struct end module Glob_lexer = struct - let parse_string _ = Error (0, "globs are not available during bootstrap") + let parse_string _ = failwith "globs are not available during bootstrap" end |} in