Nov. 9, 2023
2:14 p.m.
On 09/11/2023 10:13, Guillermo Polito wrote: [...]
## Why Ctrl-dot does not always work
not related to the topic, but may I take the opportunity to mention that ctrl-dot does not work on Linux. So this is not a solution, ever sorry for the noise nicolas
Cheers, Guille
-- Nicolas Anquetil RMod team -- Inria Lille