aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/config_lexer.mll
diff options
context:
space:
mode:
authorGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-03-03 19:02:03 +0000
committerGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-03-03 19:02:03 +0000
commit3f523f03200845e7f6e63c366dca4a62152b1974 (patch)
treee4677cedc07538468af507209659d362adf1bec4 /ide/config_lexer.mll
parent07eb98ea43ad9e3a4a4a61e883907e20bc06de37 (diff)
CoqIDE: copy/paste
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3729 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/config_lexer.mll')
-rw-r--r--ide/config_lexer.mll1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 467f68704..0d0e6307e 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -43,7 +43,6 @@ and split_list = parse
begin try
while true do
let r = next_config lb in
- prerr_endline (fst r);
result := r::!result
done
with End_of_file -> close_in ci;