aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ide_slave.ml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-22 12:55:46 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:42:01 +0200
commitb20d52da0d040fe37bb75b0b739ad7686f9af127 (patch)
tree6d8612f3a528dab9dd44add1ba26323fd8a41ce7 /ide/ide_slave.ml
parent4e84e83911c1cf7613a35b921b1e68e097f84b5a (diff)
Warning 29: non escaped end of line may be non portable
Diffstat (limited to 'ide/ide_slave.ml')
-rw-r--r--ide/ide_slave.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index ca0ef38d3..dbfe4256b 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -512,5 +512,5 @@ let () = Coqtop.toploop_init := (fun args ->
let () = Coqtop.toploop_run := loop
let () = Usage.add_to_usage "coqidetop"
-" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format
- --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n"
+" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\
+\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n"