diff options
| author | monate | 2003-05-14 12:09:29 +0000 |
|---|---|---|
| committer | monate | 2003-05-14 12:09:29 +0000 |
| commit | 05c1e8d802c326b28db14483390af2d83bd6d19a (patch) | |
| tree | 7883a437ec6cd50c9c50721fd8a116a2fd67a7b9 /ide/FAQ | |
| parent | adfffe936ed1d22f39bd12b7013447473697db74 (diff) | |
coqide: load/save file encoding support/
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/FAQ')
| -rw-r--r-- | ide/FAQ | 10 |
1 files changed, 9 insertions, 1 deletions
@@ -55,8 +55,16 @@ R6) Use coqmktop -ide -opt m1.cmx...mi.cmx Q7) How to customize the shortcuts for menus? -R6) Two solutions are offered: +R7) Two solutions are offered: - Edit $HOME/.coqide.keys by hand - Add "gtk-can-change-accels = 1" in your .coqiderc.gtk2 file. Then from CoqIde, you may select a menu entry and press the desired shortcut. Do not forget to save your preferences. + +Q8) What encoding should I use? What is this \x{iiii} in my file? +R8) The encoding option is related to the way files are saved. Keep it as UTF-8 until + it becomes important for you to exchange files with non UTF-8 aware applications. + + If you choose something else than UTF-8, then missing characters will be encoded by + \x{....} or \x{........} where the dot is a digit. The number between braces is + the hexadecimal UNICODE index for the missing character. |