diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-27 20:25:21 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-27 20:25:21 +0200 |
| commit | 78df4fe4fad46fee83f5044525fd8e530d8da6ff (patch) | |
| tree | 8d6ceedc108c46053b2f966693fb0c2e439ae39f /driver | |
| parent | 91ed1b752d2661478840e40a0d977b068d99490d (diff) | |
| download | compcert-78df4fe4fad46fee83f5044525fd8e530d8da6ff.tar.gz compcert-78df4fe4fad46fee83f5044525fd8e530d8da6ff.zip | |
More refactoring of the Debug Information.
In order to remove unnecessary dependecies the implemenation type is made
and the DebugInit file initializes the fields in the record. This allows
it to move more functions behind the Debug interface without introducing
circular dependencies.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 47d6e81c..9b1a6e70 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -683,7 +683,7 @@ let _ = Builtins.set C2C.builtins; CPragmas.initialize(); parse_cmdline cmdline_actions; - Debug.init (); (* Initialize the debug functions *) + DebugInit.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"; |