aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL.ide
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-10-13 18:30:47 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-10-13 18:30:47 +0200
commited95f122f3c68becc09c653471dc2982b346d343 (patch)
tree87e323b2d382c285e1eae864338ea397fda0923d /INSTALL.ide
parent26974a4a2301cc7b1188a3f2f29f3d3368eccc0b (diff)
Fix some typos.
Diffstat (limited to 'INSTALL.ide')
-rw-r--r--INSTALL.ide2
1 files changed, 1 insertions, 1 deletions
diff --git a/INSTALL.ide b/INSTALL.ide
index 13e741e34..6e41b2d05 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -119,5 +119,5 @@ TROUBLESHOOTING
rid of the problem is to edit by hand your coqiderc (either
/home/<user>/.config/coq/coqiderc under Linux, or
C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows)
- and replace any occurence of MOD4 by MOD1.
+ and replace any occurrence of MOD4 by MOD1.