aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cWarnings.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-01-18 15:46:23 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 00:28:53 +0200
commite8a6467545c2814c9418889201e8be19c0cef201 (patch)
tree7f513d854b76b02f52f98ee0e87052c376175a0f /lib/cWarnings.ml
parent30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff)
[location] Make location optional in Loc.located
This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
Diffstat (limited to 'lib/cWarnings.ml')
-rw-r--r--lib/cWarnings.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 4e692af36..ececc6308 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -23,7 +23,7 @@ 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 := Some loc
+let set_current_loc loc = current_loc := loc
let get_flags () = !flags