diff options
Diffstat (limited to 'utils/config.mli')
| -rw-r--r-- | utils/config.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/utils/config.mli b/utils/config.mli index d50761cebe..49ec60abe5 100644 --- a/utils/config.mli +++ b/utils/config.mli @@ -191,6 +191,10 @@ val host : string val target : string (** Whether the compiler is a cross-compiler *) +val stats : bool + (* Whether the compiler records detailed statistics about the program. + Warning: Expect a substantial performance hit. *) + val flambda : bool (** Whether the compiler was configured for flambda *) |