From 9fba2217aaea6ff676f9bffb74f82559145239f8 Mon Sep 17 00:00:00 2001
From: David Stainton <dstainton415@gmail.com>
Date: Sat, 17 Oct 2026 23:15:35 +0200
Subject: [PATCH] Fix website tagline

---
 docs/site/Main.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/site/Main.lean b/docs/site/Main.lean
index b901933..c8f3e9f 100644
--- a/docs/site/Main.lean
+++ b/docs/site/Main.lean
@@ -46,7 +46,7 @@ def front : Template := do
   pure {{
     <section class="hero">
       <h1>"Cryptlib"</h1>
-      <p class="tagline">"Cryptography for Lean 4, where a primitive's type says what must be proved about it."</p>
+      <p class="tagline">"A Lean cryptography library"</p>
       <p class="buttons">
         <a class="button" href="api/">"API reference"</a>
       </p>