diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-02 08:03:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-02 08:03:05 +0200 |
| commit | 97adfc372fd716c6701677b69950cd9279f46f27 (patch) | |
| tree | 0f0b23f778074065d8920a9c55db81d36d854833 /lib/system.mli | |
| parent | 54277abbf0fa15e0437d2a68859ceeef09ec70c3 (diff) | |
| parent | bd5da52c6c625cb4559dd92051384383473ecb1b (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/system.mli b/lib/system.mli index e1190dfb5..4dbb3695d 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -64,9 +64,11 @@ val file_exists_respecting_case : string -> string -> bool (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] - when the check fails, with the full file name. *) + when the check fails, with the full file name and expected/observed magic + numbers. *) -exception Bad_magic_number of string +type magic_number_error = {filename: string; actual: int; expected: int} +exception Bad_magic_number of magic_number_error val raw_extern_state : int -> string -> out_channel |