diff options
| author | Robert Norton | 2018-11-19 15:27:24 +0000 |
|---|---|---|
| committer | Robert Norton | 2018-11-19 15:27:24 +0000 |
| commit | b891846bef840ecbe5673c3b22cbd0f2cfceef0f (patch) | |
| tree | f40a1626b17a3cb0e373aaca925b32c938f52220 /src/util.mli | |
| parent | 1bc81fa6dcafcfe24fce3685c2eb61f882e6b65c (diff) | |
| parent | 8c2739ace6ddc9b506d8e6782a4075574115cb34 (diff) | |
Merge branch 'latex' into sail2
Diffstat (limited to 'src/util.mli')
| -rw-r--r-- | src/util.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/util.mli b/src/util.mli index 1d80bc10..fd0242a3 100644 --- a/src/util.mli +++ b/src/util.mli @@ -57,8 +57,8 @@ val opt_colors : bool ref val butlast : 'a list -> 'a list (** Mixed useful things *) -module Duplicate(S : Set.S) : sig - type dups = +module Duplicate(S : Set.S) : sig + type dups = | No_dups of S.t | Has_dups of S.elt val duplicates : S.elt list -> dups @@ -259,5 +259,7 @@ val warn : string -> unit val zencode_string : string -> string val zencode_upper_string : string -> string +val file_encode_string : string -> string + val log_line : string -> int -> string -> string val header : string -> int -> string |