summaryrefslogtreecommitdiff
path: root/Test/dafny0/ExternHelloLibrary.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/ExternHelloLibrary.cs')
-rw-r--r--Test/dafny0/ExternHelloLibrary.cs15
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.");
+ }
+ }
+}