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