From 3f40638f171f24d7c35718d7627f54bf19cad76e Mon Sep 17 00:00:00 2001
From: Wen Kokke <wen.kokke@gmail.com>
Date: Thu, 6 Sep 2018 14:48:09 +0100
Subject: [PATCH 1/4] Fix broken link in Connectives

---
 src/plfa/Connectives.lagda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plfa/Connectives.lagda b/src/plfa/Connectives.lagda
index 0803bfc0..e5dd6a82 100644
--- a/src/plfa/Connectives.lagda
+++ b/src/plfa/Connectives.lagda
@@ -1,7 +1,7 @@
 ---
 title     : "Connectives: Conjunction, disjunction, and implication"
 layout    : page
-prev      : /Isomorphisms/
+prev      : /Isomorphism/
 permalink : /Connectives/
 next      : /Negation/
 ---

From 76609c5946fb6784b0a43d3f74c15b674b297b05 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wen.kokke@gmail.com>
Date: Thu, 6 Sep 2018 15:26:50 +0100
Subject: [PATCH 2/4] Added --link-to-local-agda-names to the Makefile

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index e6d26c61..e2395567 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@ out/:
 	mkdir -p out/
 
 out/%.md: src/%.lagda | out/
-	agda2html --verbose --link-to-agda-stdlib --use-jekyll=out/ -i $< -o $@ 2>&1 \
+	agda2html --verbose --link-to-agda-stdlib --link-to-local-agda-names --use-jekyll=out/ -i $< -o $@ 2>&1 \
 		| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
 	@sed -i '1 s|---|---\nsrc       : $(<)|' $@
 

From 6fe2b851b18badc0d26d4296e5b5828f0a98d3a1 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wen.kokke@gmail.com>
Date: Thu, 6 Sep 2018 15:35:52 +0100
Subject: [PATCH 3/4] =?UTF-8?q?Added=20more=20space=20around=20the=20'=20P?=
 =?UTF-8?q?rev=20=E2=80=A2=20Source=20=E2=80=A2=20Next=20'=20buttons?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 _includes/next.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/_includes/next.html b/_includes/next.html
index 153c9d4c..24695080 100644
--- a/_includes/next.html
+++ b/_includes/next.html
@@ -1,4 +1,4 @@
-<center>
+<p style="text-align:center;">
     {% if page.prev %}
     <a alt="Previous chapter" href="{{ site.baseurl }}{{ page.prev }}">Prev</a>
     &bullet;
@@ -10,4 +10,4 @@
     &bullet;
     <a alt="Next chapter" href="{{ site.baseurl }}{{ page.next }}">Next</a>
     {% endif %}
-</center>
+</p>

From 0d580b75f97c7b27424d79883278ee572c858bbe Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Fri, 7 Sep 2018 09:59:22 +0100
Subject: [PATCH 4/4] deleted frigging

---
 src/plfa/Naturals.lagda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/plfa/Naturals.lagda b/src/plfa/Naturals.lagda
index dd2066e6..e84cd3c6 100644
--- a/src/plfa/Naturals.lagda
+++ b/src/plfa/Naturals.lagda
@@ -603,7 +603,6 @@ the 1920's.  I was told a joke: "It should be called schönfinkeling,
 but currying is tastier". Only later did I learn that the explanation
 of the misattribution was itself a misattribution.  The idea actually
 appears in the _Begriffschrift_ of Gottlob Frege, published in 1879.
-We should call it frigging!
 
 
 ## The story of creation, revisited