diff options
Diffstat (limited to 'toplevel/locality.ml')
| -rw-r--r-- | toplevel/locality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/locality.ml b/toplevel/locality.ml index 7664acbb6..03640676e 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -18,7 +18,7 @@ let check_locality locality_flag = match locality_flag with | Some b -> let s = if b then "Local" else "Global" in - CErrors.user_err "Locality.check_locality" + CErrors.user_err ~hdr:"Locality.check_locality" (str "This command does not support the \"" ++ str s ++ str "\" prefix.") | None -> () |