aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.mli
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Configuration.mli')
-rw-r--r--driver/Configuration.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index abfd3ab4..dde9d6fd 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -43,9 +43,6 @@ val has_runtime_lib: bool
val has_standard_headers: bool
(** True if CompCert's standard header files is available. *)
-val advanced_debug: bool
- (** True if advanced debug is implement for the Target *)
-
type struct_passing_style =
| SP_ref_callee (* by reference, callee takes copy *)