From b82ae19b91db32b12f0c0afe1a478f9d4caa6497 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 18 Jan 2017 12:11:46 +0100
Subject: Use quoted strings.

Instead of escaping all newlines etc for the help options use
quoted strings.
Bug 19872
---
 debug/DebugInit.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'debug')

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 =
-- 
cgit