Naïm Camille Favier
Naïm Camille Favier
What else is needed here?
I'll just cut out the middleman: the discussion happened on X/Twitter https://nitter.privacydev.net/ncfavier/status/1812145889722413267.
I can confirm that disabling headset profile autoswitching fixes the issue. Thanks for the workaround!
Here's a reproducer: ```agda -- add more cubes to increase the offset: -- 🧊 ! ``` This seems to only happen when the file contains characters outside of the [Basic...
Perhaps the [OffsetConverter](https://github.com/banacorn/agda-mode-vscode/blob/581b4e982f5518f743e46b9b05ea45be888b3c12/src/Agda.res#L236) could be reused for this?
https://github.com/banacorn/agda-mode-vscode/pull/235
Do I understand correctly that it's not possible to import agda-categories (which uses `--without-K`) from a `--cubical` module in Agda 2.6.3? This used to be possible in 2.6.2.
Oh that's much simpler lol.
Would it make sense to always adjust the offsets so that any number of arrows are spaced evenly and symmetrically? This would imply changing the offsets of existing arrows when...
@acristoffers What is your keyboard layout and what keys are you pressing to input alt+1? If you run `cat -A` in a shell and input alt+1, what is printed?