diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java index b89c3bd764e96174bede0aa806f16ba726fc7fa4..8eb569c5495dc783591d8aa79b968991f41ea4a5 100644 --- a/src/main/java/de/tla2bAst/Translator.java +++ b/src/main/java/de/tla2bAst/Translator.java @@ -37,7 +37,12 @@ import java.util.stream.Collectors; import static de.tla2b.global.TranslationGlobals.VERSION_NUMBER; public class Translator { - private static final String GENERATED_BY_TLA2B_HEADER = "/*@ generated by TLA2B "; + + /** + * This old header looks like the generated pragma which does not parse because of the text following it. + */ + private static final String GENERATED_BY_TLA2B_HEADER_OLD = "/*@ generated by TLA2B "; + private static final String GENERATED_BY_TLA2B_HEADER = "/* @generated by TLA2B "; private String parentPath; private File moduleFile; @@ -216,7 +221,8 @@ public class Translator { if (machineFile.exists()) { try (BufferedReader in = new BufferedReader(new FileReader(machineFile))) { String firstLine = in.readLine(); - if (firstLine != null && !firstLine.startsWith(GENERATED_BY_TLA2B_HEADER)) { + boolean generatedByTLA2B = firstLine != null && (firstLine.startsWith(GENERATED_BY_TLA2B_HEADER_OLD) || firstLine.startsWith(GENERATED_BY_TLA2B_HEADER)); + if (!generatedByTLA2B) { System.err.println("Error: File " + machineFile.getName() + " already exists" + " and was not generated by TLA2B.\n" + "Delete or move this file."); System.exit(-1);