diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-04 19:11:34 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-09-23 13:55:44 +0200 |
commit | efcb5cacba9bcdbd31c583ff1308a06daf56d35d (patch) | |
tree | dce30cd8c728ba6d6d202978ebc9a847a00779ea | |
parent | 32910495644e7f6fbf9b3b85ecc16f4e30447e60 (diff) | |
download | compcert-efcb5cacba9bcdbd31c583ff1308a06daf56d35d.tar.gz compcert-efcb5cacba9bcdbd31c583ff1308a06daf56d35d.zip |
Improved help messages for the -g<n> and -gdwarf-<n> options
-rw-r--r-- | debug/DebugInit.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index 9f99f08c..cfe9a6d4 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -36,14 +36,16 @@ let init () = init_none () let gnu_debugging_help = -" -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" +{| -gdwarf-2 Generate debug information in DWARF v2 format + -gdwarf-3 Generate debug information in DWARF v3 format +|} let debugging_help = {|Debugging options: -g Generate debugging information -g<n> Control generation of debugging information - (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals - without locations, <n>=3: full;) + (<n>=0: none, <n>=1: only globals, + <n>=2: globals + locals without locations, <n>=3: full) |} ^ (if Configuration.gnu_toolchain then gnu_debugging_help else "") |