aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.mli
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /ide/coqide.mli
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.mli')
-rw-r--r--ide/coqide.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.mli b/ide/coqide.mli
index d84158a0b..4c01e747a 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -9,7 +9,7 @@
(*i $Id$ i*)
(* The CoqIde main module. The following function [start] will parse the
- command line, initialize the load path, load the input
+ command line, initialize the load path, load the input
state, load the files given on the command line, load the ressource file,
produce the output state if any, and finally will launch the interface. *)