diff options
Diffstat (limited to 'library/goptions.ml')
-rw-r--r-- | library/goptions.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index b98cdac6a..db8933d28 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -36,7 +36,7 @@ type option_state = { let nickname table = String.concat " " table let error_undeclared_key key = - user_err "Goptions" (str (nickname key) ++ str ": no table or option of this type") + user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type") (****************************************************************************) (* 1- Tables *) |