aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cWarnings.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/cWarnings.ml')
-rw-r--r--lib/cWarnings.ml4
1 files changed, 0 insertions, 4 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)