diff --git a/Source/DafnyCore/dfyconfig.toml b/Source/DafnyCore/dfyconfig.toml index 66905fad48..1de176d7e6 100644 --- a/Source/DafnyCore/dfyconfig.toml +++ b/Source/DafnyCore/dfyconfig.toml @@ -1,4 +1,4 @@ -includes = ["Compilers/**/*.dfy","AST/Formatting.dfy"] +includes = ["Backends/**/*.dfy","AST/Formatting.dfy"] excludes = [] [options] diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect index 0e48bd69d3..a3ea0ba259 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/benchmarks/sequence-race/SequenceRace.dfy.expect @@ -1,8 +1,3 @@ Dafny program verifier finished with 2 verified, 0 errors -<<<<<<< HEAD -SequenceRace.dfy(35,0): Error: The benchmarking plugin does not support this translation target: Microsoft.Dafny.Compilers.CsharpCompiler (--target:cs) -Wrote textual form of partial target program to SequenceRace.cs -======= -SequenceRace.dfy(35,0): Error: The benchmarking plugin does not support this compilation target: Microsoft.Dafny.Compilers.CsharpCompiler (--target:cs) ->>>>>>> origin/master +SequenceRace.dfy(35,0): Error: The benchmarking plugin does not support this translation target: Microsoft.Dafny.Compilers.CsharpCodeGenerator (--target:cs) diff --git a/docs/HowToFAQ/make-error-catalog b/docs/HowToFAQ/make-error-catalog index 42b2993d15..7336b26ef1 100755 --- a/docs/HowToFAQ/make-error-catalog +++ b/docs/HowToFAQ/make-error-catalog @@ -4,7 +4,7 @@ cd "$dir" FAIL=0 java MakeErrorCatalog.java Errors-Compiler.template \ - ../../Source/DafnyCore/Compilers/CompilerErrors.cs + ../../Source/DafnyCore/Backends/GeneratorErrors.cs if [ "$?" != "0" ] ; then echo "Java build-run failed"; exit 1; fi diff Errors-Compiler.tmp Errors-Compiler.md || \