diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-11-16 16:50:45 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-11-16 16:50:45 +0100 |
| commit | 1f51841a41b98ecaed25d84c848fc161d8d18e2a (patch) | |
| tree | 7cb05737e8edebd932c047a2948fe16ef3c4d8d2 /driver/Clflags.ml | |
| parent | 20e3c4aee0332960b008ec7aaa5c8689fa0bd059 (diff) | |
| download | compcert-1f51841a41b98ecaed25d84c848fc161d8d18e2a.tar.gz compcert-1f51841a41b98ecaed25d84c848fc161d8d18e2a.zip | |
Added now option to control debug output.
The new option gdepth subumes the gonly-globals. The option
allows it to control the level of information that is produced.
This option allows it to generate debugging inforation for:
-Only globals
-Global and local variables but without location information for
the local variable
-Full information
Bug 17638.
Diffstat (limited to 'driver/Clflags.ml')
| -rw-r--r-- | driver/Clflags.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 1eaa5449..6c2cc661 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -47,7 +47,7 @@ let option_dasm = ref false let option_sdump = ref false let option_g = ref false let option_gdwarf = ref 2 -let option_gglobal = ref false +let option_gdepth = ref 3 let option_o = ref (None: string option) let option_E = ref false let option_S = ref false |