more changes

.gitignore

@@ -1,2 +1,3 @@
 *.agdai
 .direnv/
+public/

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 \{\} \;
 

src/Everything.agda

@@ -0,0 +1,5 @@
+import Intro
+import Intro
+import Intro
+import Intro
+import Intro

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