diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-01-18 12:11:46 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-01-18 12:11:46 +0100 |
commit | b82ae19b91db32b12f0c0afe1a478f9d4caa6497 (patch) | |
tree | 085e83886bdeddd71959a89de96dfad85a47ed12 /debug/DebugInit.ml | |
parent | 1e26e3d26fa06c38f712ff4a2554de76212d38ab (diff) | |
download | compcert-b82ae19b91db32b12f0c0afe1a478f9d4caa6497.tar.gz compcert-b82ae19b91db32b12f0c0afe1a478f9d4caa6497.zip |
Use quoted strings.
Instead of escaping all newlines etc for the help options use
quoted strings.
Bug 19872
Diffstat (limited to 'debug/DebugInit.ml')
-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 = |