diff options
Diffstat (limited to 'parsing/location.ml')
| -rw-r--r-- | parsing/location.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/location.ml b/parsing/location.ml index a0a52bfc0..1bdc67f13 100644 --- a/parsing/location.ml +++ b/parsing/location.ml @@ -90,7 +90,7 @@ let rec highlight_locations loc1 loc2 = (* Print the location in some way or another *) -open Format +open Formatmsg let reset () = num_loc_lines := 0 |