[Gretl-devel] glitch with switching decimal separator

Hi, with a snapshot from March 11th, it seems that when (running in German which natively would have a decimal comma) I switch off the comma in the settings, it works, but when I try to switch it back _on_, then the decimal point stays. Only a gretl restart corrects the issue. (Actually I seem to remember that a restart was always required in the past, but I'm not getting that alert message here.)  I'm talking about small scripts in the script editor which print out decimal numbers. thanks sven