From 114702126feca8c6615602ec093309bf4c7869b5 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 7 Dec 2018 13:21:05 +0100 Subject: [PATCH] Fix some typos in Editors.md. --- Editor.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Editor.md b/Editor.md index da129f9dd..4f8ed84ad 100644 --- a/Editor.md +++ b/Editor.md @@ -95,12 +95,12 @@ results in a decent choice for the symbols used in Iris: CoqIDE does not have support for unicode itself, but you can use the Intelligent Input Bus (IBus) framework for multilingual input. First, install `ibus-m17n` -via your system's package manager. Next, create a file `~/.m17n.d/coq.min` to +via your system's package manager. Next, create a file `~/.m17n.d/coq.mim` to configure an input method based on the math symbol list, and with some custom aliases for symbols used a lot in Iris: ``` -;; Usage: copy to ~/.m17n.d/coq.min +;; Usage: copy to ~/.m17n.d/coq.mim (input-method t coq) (description "Input method for Coq") @@ -210,8 +210,9 @@ aliases for symbols used a lot in Iris: To use this input method, you should: -1. Enable it using the IBus configuration tool (there are different versions of - the configuration tool depending on the desktop you are using). The "Coq" - input method will typically appear in the category "other". -2. In CoqIDE, you can now use the input method by performing a right click, - and selecting "System (IBus)" under "input method". +1. Enable the "Coq" input using your system settings or using the IBus + configuration tool. The Coq input method typically appears in the category + "other". +2. On some systems: In CoqIDE, you have to enable the input method by performing + a right click on the text area, and selecting "System (IBus)" under "input + method". -- GitLab