diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/misctypes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index b9f5a6dbe2..e8164c02d6 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -37,7 +37,7 @@ type 'id move_location = (** Sorts *) -type sort_info = Pp.std_ppcmds option +type sort_info = string option type glob_sort = GProp | GSet | GType of sort_info (** Casts *) |