chore: move to github?

the1lab · Dec 5, 2021 · 0713a7d · 0713a7d
1 parent 6e87791
commit 0713a7d
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 37 deletions.
diff --git a/.gitattributes b/.gitattributes
@@ -1 +1 @@
-*.lagda.md gitlab-language=agda
+*.lagda.md text diff=agda linguist-language=agda
diff --git a/.github/workflows/buid.yml b/.github/workflows/buid.yml
@@ -0,0 +1,9 @@
+name: Build 1Lab
+on: [push, pull_request]
+jobs:
+  container:
+    runs-on: ubuntu-latest
+    container: pltamy/1lab:latest
+    steps:
+      - run: 1lab-shake all -j
+        name: Type check and build
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
diff --git a/.gitlab/merge_request_templates/MR.md b/.gitlab/merge_request_templates/MR.md
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		*.lagda.md gitlab-language=agda
		*.lagda.md text diff=agda linguist-language=agda