aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-12 20:20:15 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-12 20:20:15 +0200
commit424cffe91ee8819de8cde27d98c534eed51ca251 (patch)
tree7cb695d8478f69694e1d7a51ff16c679204f819a /lib
parentde828ea7d9991d4509156ce2ae073011998e65b5 (diff)
parent2dbb54b1bc3967ee5d6e838cce8c56b88bd9477d (diff)
Merge PR #7194: [warnings] Remove `set_current_loc` hack.
Diffstat (limited to 'lib')
-rw-r--r--lib/cWarnings.ml4
-rw-r--r--lib/cWarnings.mli2
2 files changed, 0 insertions, 6 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 92c86eaea..fda25a0a6 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -22,11 +22,8 @@ type t = {
let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
-let current_loc = ref None
let flags = ref ""
-let set_current_loc loc = current_loc := loc
-
let get_flags () = !flags
let add_warning_in_category ~name ~category =
@@ -170,7 +167,6 @@ let create ~name ~category ?(default=Enabled) pp =
set_flags !flags;
fun ?loc x ->
let w = Hashtbl.find warnings name in
- let loc = Option.append loc !current_loc in
match w.status with
| Disabled -> ()
| AsError -> CErrors.user_err ?loc (pp x)
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index fa96b18c8..f97a53c4d 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -10,8 +10,6 @@
type status = Disabled | Enabled | AsError
-val set_current_loc : Loc.t option -> unit
-
val create : name:string -> category:string -> ?default:status ->
('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit