aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorslb Prime2021-02-28 00:22:01 -0500
committerGitHub2021-02-28 00:22:01 -0500
commitddd4ffea1dd58cd3e50c188699684b7506ce3bee (patch)
tree3967612b2933809457ad509848d2af6e3661e44f /doc
parentca38bf53deed39c716a911b8d288f91eb334452e (diff)
Fix link of default_bindings.
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/practical-tools/coqide.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index dcc60195ed..e7237cf7eb 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -248,7 +248,7 @@ right arrow, or ``\>=`` for a greater than or equal sign.
A larger number of latex tokens are supported by default. The full list
is available here:
-https://github.com/coq/coq/blob/master/ide/default_bindings_src.ml
+https://github.com/coq/coq/blob/master/ide/coqide/default_bindings_src.ml
Custom bindings may be added, as explained further on.