diff options
| author | Théo Zimmermann | 2019-04-19 18:52:26 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-04-30 16:10:17 +0200 |
| commit | 890f206ebea4a14f5be8b273cee4ae8f99ca25e1 (patch) | |
| tree | 5133e28834b5d16ff88fda3212be3f14bf6d8c22 /doc/sphinx/practical-tools | |
| parent | bb4b9469ddf45d76385cdcddf27dc82266a8c73b (diff) | |
Split changes between main changes and other changes (no repetition).
Add more links to PRs and credits of authors.
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 97d86943fb..6cbd00f45d 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -252,6 +252,8 @@ use antialiased fonts or not, by setting the environment variable `GDK_USE_XFT` to 1 or 0 respectively. +.. _coqide-unicode: + Bindings for input of Unicode symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |