aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-09-04 19:11:34 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2022-09-23 13:55:44 +0200
commitefcb5cacba9bcdbd31c583ff1308a06daf56d35d (patch)
treedce30cd8c728ba6d6d202978ebc9a847a00779ea
parent32910495644e7f6fbf9b3b85ecc16f4e30447e60 (diff)
downloadcompcert-efcb5cacba9bcdbd31c583ff1308a06daf56d35d.tar.gz
compcert-efcb5cacba9bcdbd31c583ff1308a06daf56d35d.zip
Improved help messages for the -g<n> and -gdwarf-<n> options
-rw-r--r--debug/DebugInit.ml8
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 "")