From 01ebc0a3155d700979fd962c819627b1184cc662 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 24 Apr 2024 12:46:02 +0200
Subject: [PATCH] more changes

---
 .gitignore          | 3 ++-
 Makefile            | 4 ++--
 src/Everything.agda | 5 +++++
 src/Intro.lagda.md  | 1 +
 4 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/.gitignore b/.gitignore
index e916b52..c9b3fcc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
 *.agdai
-.direnv/
\ No newline at end of file
+.direnv/
+public/
diff --git a/Makefile b/Makefile
index 42a7ab1..c48f538 100644
--- a/Makefile
+++ b/Makefile
@@ -9,12 +9,12 @@ pandoc: public/*.md
 	)
 
 agda: Everything.agda
-	agda --html --html-dir=public src/Everything.agda --html-highlight=auto -i.
+	agda --html --html-dir=public src/Everything.agda --html-highlight=auto -isrc
 	rm -f public/Agda.css
 	cp Agda.css public/Agda.css
 
 clean:
-	rm -f Everything.agda
+	rm -f src/Everything.agda
 	rm -rf public/*
 	find . -name '*.agdai' -exec rm \{\} \;
 
diff --git a/src/Everything.agda b/src/Everything.agda
index e69de29..20ef564 100644
--- a/src/Everything.agda
+++ b/src/Everything.agda
@@ -0,0 +1,5 @@
+import Intro
+import Intro
+import Intro
+import Intro
+import Intro
diff --git a/src/Intro.lagda.md b/src/Intro.lagda.md
index f7b4492..c0bd29e 100644
--- a/src/Intro.lagda.md
+++ b/src/Intro.lagda.md
@@ -6,6 +6,7 @@ Das sind Typen welche von Termen der Programmiersprache abhängen können, aber
 
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 module Intro where
 Type = Set
 private