aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2011-04-21 16:16:01 +0000
committerletouzey2011-04-21 16:16:01 +0000
commit12cf5007bbc2b8c6af5cd9cb2cb7fc882b40f623 (patch)
tree543be9114e8f129b00c2a664540aa662634aea03
parent00951f509d8a729420cedef3d6e27672866b2c5c (diff)
Coqide: typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14046 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/coqide.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 63754fd510..2ab9cd9669 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -698,7 +698,7 @@ object(self)
img#set_stock `DIALOG_WARNING;
img#set_icon_size `DIALOG;
img#coerce)
- ("File "^f^"already exists")
+ ("File "^f^" already exists")
)
with 1 -> self#save f
| _ -> false