# HG changeset patch # User wenzelm # Date 1483346485 -3600 # Node ID ba0d4829d5f14650e433e29612f1acbbd6969540 # Parent ebaf9d01a9645763bb83353220905b8db48700e2 tuned; diff -r ebaf9d01a964 -r ba0d4829d5f1 src/Tools/VSCode/src/grammar.scala --- a/src/Tools/VSCode/src/grammar.scala Mon Jan 02 09:39:00 2017 +0100 +++ b/src/Tools/VSCode/src/grammar.scala Mon Jan 02 09:41:25 2017 +0100 @@ -146,6 +146,6 @@ val output_path = output getOrElse Path.explode(default_output(logic)) Output.writeln(output_path.implode) - File.write(output_path, generate(keywords)) + File.write_backup(output_path, generate(keywords)) }) }