Open andreh7 opened 8 years ago
when saving the workspace data with the --save command line option, the program should check whether the output format is known (from the extension) BEFORE reading the workspace (which can take a long time).
when saving the workspace data with the --save command line option, the program should check whether the output format is known (from the extension) BEFORE reading the workspace (which can take a long time).