From ba8f610c0a611c98911afc2d79214fde91cb4143 Mon Sep 17 00:00:00 2001
From: Cole Schlesinger <cole@galois.com>
Date: Thu, 14 Nov 2024 07:24:43 -0800
Subject: [PATCH] Remove empty stub pages

---
 docs/README.md                      | 4 ++--
 docs/getting-started/hello-world.md | 4 ----
 docs/help/README.md                 | 4 ----
 docs/testing/README.md              | 4 ----
 docs/verification/README.md         | 4 ----
 mkdocs.yml                          | 7 -------
 6 files changed, 2 insertions(+), 25 deletions(-)
 delete mode 100644 docs/getting-started/hello-world.md
 delete mode 100644 docs/help/README.md
 delete mode 100644 docs/testing/README.md
 delete mode 100644 docs/verification/README.md

diff --git a/docs/README.md b/docs/README.md
index 20cca88..6e21abc 100644
--- a/docs/README.md
+++ b/docs/README.md
@@ -28,10 +28,10 @@ appreciated!
 
     ---
 
-    Check out the Hello World tutorial to write, test, and verify your first
+    Check out the *Basic Usage* tutorial to write, test, and verify your first
     spec
 
-    [:octicons-arrow-right-24: Hello World](getting-started/hello-world.md)
+    [:octicons-arrow-right-24: Basic Usage](getting-started/tutorials/basic-usage.md)
 
 -   :material-format-font:{ .lg .middle } __Tutorials__
 
diff --git a/docs/getting-started/hello-world.md b/docs/getting-started/hello-world.md
deleted file mode 100644
index 158804d..0000000
--- a/docs/getting-started/hello-world.md
+++ /dev/null
@@ -1,4 +0,0 @@
-# Hello World
-
-!!! TODO
-    This page is under construction.
diff --git a/docs/help/README.md b/docs/help/README.md
deleted file mode 100644
index ecbedc0..0000000
--- a/docs/help/README.md
+++ /dev/null
@@ -1,4 +0,0 @@
-# Help
-
-!!! TODO
-    This page is under construction.
diff --git a/docs/testing/README.md b/docs/testing/README.md
deleted file mode 100644
index 567cc68..0000000
--- a/docs/testing/README.md
+++ /dev/null
@@ -1,4 +0,0 @@
-# Testing
-
-!!! TODO
-    This page is under construction.
diff --git a/docs/verification/README.md b/docs/verification/README.md
deleted file mode 100644
index e71fbd8..0000000
--- a/docs/verification/README.md
+++ /dev/null
@@ -1,4 +0,0 @@
-# Verification
-
-!!! TODO
-    This page is under construction.
diff --git a/mkdocs.yml b/mkdocs.yml
index 04c4963..08433ec 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -98,7 +98,6 @@ nav:
   - Getting started:
     - README.md
     - Installation: getting-started/installation.md
-    - "Hello world": getting-started/hello-world.md
     - Tutorials:
       - getting-started/tutorials/README.md
       - "Basic usage": getting-started/tutorials/basic-usage.md
@@ -131,12 +130,6 @@ nav:
     - Scoping: specifications/scoping.md
     - "Tactics (proof hints)": specifications/tactics.md
     - Interactive theorem proving: specifications/interactive-theorem-proving.md
-  - Testing:
-    - testing/README.md
-  - Verification:
-    - verification/README.md
   - Reference:
     - reference/README.md
-  - Help:
-    - help/README.md