diff options
| -rw-r--r-- | INSTALL.ide | 14 | ||||
| -rw-r--r-- | doc/faq/FAQ.tex | 9 |
2 files changed, 23 insertions, 0 deletions
diff --git a/INSTALL.ide b/INSTALL.ide index 029ec03ce7..5a4a622386 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -115,3 +115,17 @@ There are three configuration files located in your $(HOME) dir. to change the default shortcuts for the menus. Read ide/FAQ for more informations. + + +TROUBLESHOOTING + + - Problem with automatic templates + + Some users may experiment problems with unwanted automatic + templates while using Coqide. This is due to a change in the + modifiers keys available through GTK. The straightest way to get + rid of the problem is to edit by hand your .coqiderc (either + /home/<user>/.coqiderc under Linux, or + C:\Documents and Settings\<user>\.coqiderc under Windows) + and replace any occurence of MOD4 by MOD1. + diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index f40c28c4d4..0644cf369a 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2350,6 +2350,15 @@ Glib.Utf8.from_unichar 0x2200;; The number between braces is the hexadecimal UNICODE index for the missing character. +\Question{How to get rid of annoying unwanted automatic templates?} + +Some users may experiment problems with unwanted automatic +templates while using Coqide. This is due to a change in the +modifiers keys available through GTK. The straightest way to get +rid of the problem is to edit by hand your .coqiderc (either +\verb|/home/<user>/.coqiderc| under Linux, or \\ +\verb|C:\Documents and Settings\<user>\.coqiderc| under Windows) + and replace any occurence of \texttt{MOD4} by \texttt{MOD1}. |