Closed gdementen closed 2 years ago
fix critical bug which made the editor impossible to start after having used the demonstration dataset (#232), implement resizing editor columns when changing the number of digits (#145) and misc other cleanups and maintenance work (including #212)
I am going to merge this as there is no change to the API
fix critical bug which made the editor impossible to start after having used the demonstration dataset (#232), implement resizing editor columns when changing the number of digits (#145) and misc other cleanups and maintenance work (including #212)