summaryrefslogtreecommitdiff
path: root/Source/DafnyDriver
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2011-02-27 00:20:54 +0000
committerGravatar rustanleino <unknown>2011-02-27 00:20:54 +0000
commit7428deb21f108ea296501001bdc8eef92b281a5a (patch)
treefdb4e876911c0e60cdca16398377ca5807365d8a /Source/DafnyDriver
parenta922ff73e833037aa49e0cdb149be63bba90484d (diff)
Dafny: Non-empty Visual-Studio error messages for related split-expr locations.
Dafny: Forbid jumps from ghost code.
Diffstat (limited to 'Source/DafnyDriver')
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index b3efd7aa..aa0be9dd 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -268,7 +268,7 @@ namespace Microsoft.Boogie
}
if (tok is Dafny.NestedToken) {
var nt = (Dafny.NestedToken)tok;
- ReportBplError(nt.Inner, "Related location", false);
+ ReportBplError(nt.Inner, "Related location: Related location", false);
}
}