aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorBenjamin Barenblat2018-07-22 18:19:26 -0400
committerHugo Herbelin2018-10-15 13:28:52 +0200
commit06cd051d140a183229cd43f0bbae152d6ad8d6ca (patch)
tree6528aa85924d1cfdb965b81a15b4ec93189554fa /ide
parentecf999c8f8a677508d2856c3c8a7cacfa5da3839 (diff)
Correct some spelling errors
Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
Diffstat (limited to 'ide')
-rw-r--r--ide/nanoPG.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index 2be5dce426..002722ace9 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -189,7 +189,7 @@ let emacs = insert emacs "Emacs" [] [
run "Edit" "Cut";
{ s with kill = Some(txt,false); sel = false }
else s));
- mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ ->
+ mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ ->
let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
let k =
if i#ends_line then begin