aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/ErrorReports.ml
diff options
context:
space:
mode:
authorFrançois Pottier <francois.pottier@inria.fr>2015-10-28 13:20:40 +0100
committerFrançois Pottier <francois.pottier@inria.fr>2015-10-28 13:20:40 +0100
commit0e9ce30b09291812b14230f14a0614a2deee47a7 (patch)
tree3a440c3ec6a534c29e63bc3ef18c10eeb4472a4a /cparser/ErrorReports.ml
parent45efec6f22978d18e73f7dd7be29439d16bd180c (diff)
downloadcompcert-kvx-0e9ce30b09291812b14230f14a0614a2deee47a7.tar.gz
compcert-kvx-0e9ce30b09291812b14230f14a0614a2deee47a7.zip
Set [ErrorReports.debug] to [false].
When [debug] is [false], there are a few places where we silently ignore an error. This should not make any difference if everything works as planned.
Diffstat (limited to 'cparser/ErrorReports.ml')
-rw-r--r--cparser/ErrorReports.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/ErrorReports.ml b/cparser/ErrorReports.ml
index a271ece1..4bbf3ded 100644
--- a/cparser/ErrorReports.ml
+++ b/cparser/ErrorReports.ml
@@ -24,7 +24,7 @@ module S = MenhirLib.General (* Streams *)
silently cover up for our internal error. Thus, we typically use an idiom of
the form [if debug then assert false else <some default value>]. *)
-let debug = true
+let debug = false
(* -------------------------------------------------------------------------- *)