Normalise line endings using a .gitattributes file. Unfortunately

this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.

1 files changed, 21 insertions, 21 deletions

diff --git a/Test/test0/Orderings.bpl b/Test/test0/Orderings.bpl
index 0d55ed27..1cf900b6 100644
--- a/Test/test0/Orderings.bpl
+++ b/Test/test0/Orderings.bpl
@@ -1,22 +1,22 @@
-// RUN: %boogie -noVerify "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-

-type C;

-

-const c:int extends a;

-const d:int extends a complete;

-const e:int extends unique a, b;

-const f:int extends complete;

-

-const a:int;

-const b:int;

-

-const g:int extends x;        // error: undeclared parent

-

-const c0:C;

-const c1:C extends c0, c0;    // error: parent mentioned twice

-const c2:C extends c2;        // error: constant as its own parent

-

-const h:int extends y;        // error: variable cannot be parent

-

+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type C;
+
+const c:int extends a;
+const d:int extends a complete;
+const e:int extends unique a, b;
+const f:int extends complete;
+
+const a:int;
+const b:int;
+
+const g:int extends x;        // error: undeclared parent
+
+const c0:C;
+const c1:C extends c0, c0;    // error: parent mentioned twice
+const c2:C extends c2;        // error: constant as its own parent
+
+const h:int extends y;        // error: variable cannot be parent
+
 var y:int;
\ No newline at end of file