summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2022-12-08 10:33:21 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2022-12-08 10:35:16 +0000
commit4fa5948dafdb102ad0ab1cd3753d910929534673 (patch)
tree98c542ce291dc4942bc506f5be2b28b0604ba15e
Initial commit.
-rw-r--r--.gitignore1
-rw-r--r--obs.ipkg5
-rw-r--r--src/Obs.idr0
3 files changed, 6 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..84c048a
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/build/
diff --git a/obs.ipkg b/obs.ipkg
new file mode 100644
index 0000000..4a5cafc
--- /dev/null
+++ b/obs.ipkg
@@ -0,0 +1,5 @@
+package obs
+authors = "Greg Brown"
+sourcedir = "src"
+
+modules = Obs
diff --git a/src/Obs.idr b/src/Obs.idr
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/Obs.idr