diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /ide/coqide.mli | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (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.mli | 2 |
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. *) |