Merge commit 'df5c5f5'

1 files changed, 15 insertions, 0 deletions

diff --git a/Test/dafny0/ExternHelloLibrary.cs b/Test/dafny0/ExternHelloLibrary.cs
new file mode 100644
index 00000000..81163997
--- /dev/null
+++ b/Test/dafny0/ExternHelloLibrary.cs
@@ -0,0 +1,15 @@
+// Note that  ExternHelloLibrary.dll was produced from this file using
+// csc /t:library ExternHelloLibrary.cs 
+
+using System;
+
+namespace ExternHelloLibrary
+{
+  public static class ExternHelloLibrary
+  {
+    public static void SayHello()
+    {
+      Console.WriteLine("Hello from ExternHelloLibrary.");
+    }
+  }
+}