diff options
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/DebugInit.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index ed22f7c2..94a8cf02 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -71,11 +71,12 @@ let gnu_debugging_help = " -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" let debugging_help = -"Debugging options:\n\ -\ -g Generate debugging information\n\ -\ -g<n> Control generation of debugging information\n\ -\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals \n\ -\ without locations, <n>=3: full;)\n" +{|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;) +|} ^ (if gnu_system then gnu_debugging_help else "") let gnu_debugging_actions = |