06-07-2021, 12:28 PM
I have finished some remote games and restarted Ludii. I click on "Reset Names to Defaults" and it just sort of flashes. But the old remote names are still there. The checkbox is not checked. (The remote game was actually on 1.1.16 if that makes a difference.) Changing them manually and pressing Apply does work.