phikal
phikal
Oh, my bad. What kind of help could you need?
My prompt is just a dollar sign, and this occurs locally. That being said, I do notice that the issue appears to disappear when I rename my `.bashrc` to something...
https://github.com/agda/agda/pull/8181 can fix this by adjusting `xref-backend-functions`, but note the by default M-. will display the source buffer in the same window as the information buffer was using.
That makes sense, I can take a look at splitting the commit up over the weekend. But here, as with all the other changes there is no hurry (though it...
I've split up the commits, and actually found a few more things to improve over my initial suggestion a few years back. The `agda-input-process-translations` is the most important change here,...
When using `git add -p` I also noticed this change that I couldn't explain: ```diff diff --git a/src/data/emacs-mode/agda-input.el b/src/data/emacs-mode/agda-input.el index f7233e8e4d..2c583dfb18 100644 --- a/src/data/emacs-mode/agda-input.el +++ b/src/data/emacs-mode/agda-input.el @@ -229,6 +229,7 @@...
Depending on how they generate the bindings, it shouldn't be difficult to adjust the translation. The mapping remains a regular Elisp variable, that any (Elisp) script can utilise. On 12...
> Does this change affect the user interface? If there are multiple translations for a single key sequence, then it matters in what order those translations are added. If you...
> You can find all key sequences with multiple translations by running the command agda-input-show-translations (see the end of the buffer). I'll check that out. > Copying those bindings to...