diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 4238d9af..a81ec052 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -952,7 +952,8 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string = in log#serror err; if !Config.extract_fail_hard then raise (Failure err) - else "(ERROR: \"" ^ id_to_string id ctx ^ "\")") + else + "(%%%ERROR: unknown identifier\": " ^ id_to_string id ctx ^ "\"%%%)") else let m = ctx.names_map.id_to_name in match IdMap.find_opt id m with |