1 files changed, 6 insertions, 0 deletions
diff --git a/libpintos-rs/src/lib.rs b/libpintos-rs/src/lib.rs
new file mode 100644
index 0000000..2ad4657
--- /dev/null
+++ b/libpintos-rs/src/lib.rs
@@ -0,0 +1,6 @@
+#![no_std]
+
+#[link(name="pintos", kind="static")]
+extern {
+    pub fn exit(status: i32);
+}