diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-16 11:10:28 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-16 11:10:28 +0200 |
commit | 3344bcf59acb1ae8d43a0d15acb4b824689e706d (patch) | |
tree | a5621a5d30ee7e39e2e6d2a95e02ab018e8ef846 /driver/Driver.ml | |
parent | 36fe88d4cc2022947474a2fcc0b650e22f41ee3e (diff) | |
download | compcert-3344bcf59acb1ae8d43a0d15acb4b824689e706d.tar.gz compcert-3344bcf59acb1ae8d43a0d15acb4b824689e706d.zip |
Add the debug interface file.
The new file Debug.ml contains the interface for generating and
printing debug information. In order to generate debug information
the init function initializes the necessary functions depending
on the -g flag. If the -g is not there all functions are dummy
functions which do nothing.
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r-- | driver/Driver.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index f53de821..04acf902 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -682,6 +682,7 @@ let _ = Builtins.set C2C.builtins; CPragmas.initialize(); parse_cmdline cmdline_actions; + Debug.init (); (* Initialize the debug functions *) let nolink = !option_c || !option_S || !option_E || !option_interp in if nolink && !option_o <> None && !num_source_files >= 2 then begin eprintf "Ambiguous '-o' option (multiple source files)\n"; |