aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index c1555e57f..e8e925e44 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -54,7 +54,7 @@ let rec read_all_lines in_chan =
let arg = input_line in_chan in
let len = String.length arg in
let arg =
- if arg.[len - 1] = '\r' then
+ if len > 0 && arg.[len - 1] = '\r' then
String.sub arg 0 (len - 1)
else arg
in