Skip to content

Commit

Permalink
Fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
keyboardDrummer committed Feb 20, 2024
1 parent 0cdbacc commit ad596d6
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 8 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore/dfyconfig.toml
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
includes = ["Compilers/**/*.dfy","AST/Formatting.dfy"]
includes = ["Backends/**/*.dfy","AST/Formatting.dfy"]
excludes = []

[options]
Expand Down
Original file line number Diff line number Diff line change
@@ -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)
2 changes: 1 addition & 1 deletion docs/HowToFAQ/make-error-catalog
Original file line number Diff line number Diff line change
Expand Up @@ -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 || \
Expand Down

0 comments on commit ad596d6

Please sign in to comment.