From c579e503686cbfac87c2a43e90f551ff196df68d Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 12 Apr 2024 09:47:32 +0200
Subject: [PATCH] some webpage reorganization

---
 docs/_config.yml           |  6 +++---
 docs/_layouts/default.html |  2 +-
 docs/index.md              | 10 ++--------
 3 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/docs/_config.yml b/docs/_config.yml
index 012821d..5c35fbd 100644
--- a/docs/_config.yml
+++ b/docs/_config.yml
@@ -18,11 +18,11 @@
 # You can create any custom variable you would like, and they will be accessible
 # in the templates via {{ site.myvariable }}.
 
-title: Bonn Analysis Seminar
+title: Collaborative Formalization of Analysis
 #email: your-email@example.com
-description: A formalization in Lean 4
+description: Bonn Seminar on formalizing Fourier analysis in Lean 4
 baseurl: "" # the subpath of your site, e.g. /blog
-url: "https://fpvandoorn.github.io/BonnAnalysis/" # the base hostname & protocol for your site, e.g. http://example.com
+url: "https://florisvandoorn.com/BonnAnalysis/" # the base hostname & protocol for your site, e.g. http://example.com
 #twitter_username: jekyllrb
 github_username: fpvandoorn
 repository: fpvandoorn/BonnAnalysis
diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html
index a80f3d0..02e1feb 100644
--- a/docs/_layouts/default.html
+++ b/docs/_layouts/default.html
@@ -28,8 +28,8 @@ <h1 class="project-name">{{ page.title | default: site.title | default: site.git
     <h2 class="project-tagline">{{ page.description | default: site.description | default: site.github.project_tagline
       }}</h2>
     <a href="blueprint" class="btn">Blueprint</a>
+    <a href="blueprint.pdf" class="btn">Blueprint (pdf)</a>
     <a href="docs" class="btn">Documentation</a>
-    <a href="blueprint.pdf" class="btn">Paper</a>
     {% if site.github.is_project_page %}
     <a href="{{ site.github.repository_url }}" class="btn">View on GitHub</a>
     {% endif %}
diff --git a/docs/index.md b/docs/index.md
index 92c3d88..8016823 100644
--- a/docs/index.md
+++ b/docs/index.md
@@ -10,9 +10,7 @@ usemathjax: true
 
 # Bonn Analysis Seminar
 
-* [Blueprint of the proof](https://florisvandoorn.com/BonnAnalysis/blueprint/)
-* [Blueprint (pdf)](https://florisvandoorn.com/BonnAnalysis/blueprint.pdf)
-* [Documentation of the methods](https://florisvandoorn.com/BonnAnalysis/docs/)
+We will formalize results in Fourier analysis, such as Plancherel's theorem and the interpolation theorems.
 
 ## Build the Lean files
 
@@ -21,11 +19,7 @@ See [the installation instructions](https://leanprover-community.github.io/get_s
 
 To build the project, run `lake exe cache get` and then `lake build`.
 
-## Build the blueprint
-
-The blueprint is automatically built on each push to the project.
-You can test whether the build is working by building the pdf locally:
-`xelatex blueprint/src/print.tex`.
+For more detailed build and contribution instructions see the Github README.
 
 <!-- To build the web version of the blueprint locally, you need a working LaTeX installation.
 Furthermore, you need some packages: