fix: Backport additional Jekyll changes (#39)

Same as dafny-lang/dafny#5014
dafny-lang · Feb 21, 2024 · 73da6bd · 73da6bd
1 parent e5073ce
commit 73da6bd
Show file tree

Hide file tree

Showing 17 changed files with 80 additions and 12 deletions.
diff --git a/latest/StyleGuide/Style-Guide.md b/latest/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/latest/VerificationOptimization/VerificationOptimization.md b/latest/VerificationOptimization/VerificationOptimization.md
@@ -1,3 +1,7 @@
+---
+title: Verification Optimization
+---
+
 # Overview
 
 Dafny verifies your program using a type of theorem prover known as a Satisfiability Modulo Theories (SMT) solver. More specifically, it uses the [Z3](https://github.com/Z3Prover/z3) solver. In many cases, it's possible to state only the final properties you want your program to have, with annotations such as `requires` and `ensures` clauses, and let the prover do the rest for you, automatically.

diff --git a/v3.10.0/StyleGuide/Style-Guide.md b/v3.10.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v3.11.0/StyleGuide/Style-Guide.md b/v3.11.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v3.12.0/StyleGuide/Style-Guide.md b/v3.12.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v3.13.1/StyleGuide/Style-Guide.md b/v3.13.1/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v3.9.0/StyleGuide/Style-Guide.md b/v3.9.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v3.9.1/StyleGuide/Style-Guide.md b/v3.9.1/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v4.0.0/StyleGuide/Style-Guide.md b/v4.0.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v4.1.0/StyleGuide/Style-Guide.md b/v4.1.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v4.1.0/VerificationOptimization/VerificationOptimization.md b/v4.1.0/VerificationOptimization/VerificationOptimization.md
@@ -1,3 +1,7 @@
+---
+title: Verification Optimization
+---
+
 # Overview
 
 Dafny verifies your program using a type of theorem prover known as a Satisfiability Modulo Theories (SMT) solver. More specifically, it uses the [Z3](https://github.com/Z3Prover/z3) solver. In many cases, it's possible to state the only the final properties you want your program to have, with annotations such as `requires` and `ensures` clauses, and let the prover do the rest for you, automatically.

diff --git a/v4.2.0/StyleGuide/Style-Guide.md b/v4.2.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v4.2.0/VerificationOptimization/VerificationOptimization.md b/v4.2.0/VerificationOptimization/VerificationOptimization.md
@@ -1,3 +1,7 @@
+---
+title: Verification Optimization
+---
+
 # Overview
 
 Dafny verifies your program using a type of theorem prover known as a Satisfiability Modulo Theories (SMT) solver. More specifically, it uses the [Z3](https://github.com/Z3Prover/z3) solver. In many cases, it's possible to state only the final properties you want your program to have, with annotations such as `requires` and `ensures` clauses, and let the prover do the rest for you, automatically.

diff --git a/v4.3.0/StyleGuide/Style-Guide.md b/v4.3.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v4.3.0/VerificationOptimization/VerificationOptimization.md b/v4.3.0/VerificationOptimization/VerificationOptimization.md
@@ -1,3 +1,7 @@
+---
+title: Verification Optimization
+---
+
 # Overview
 
 Dafny verifies your program using a type of theorem prover known as a Satisfiability Modulo Theories (SMT) solver. More specifically, it uses the [Z3](https://github.com/Z3Prover/z3) solver. In many cases, it's possible to state only the final properties you want your program to have, with annotations such as `requires` and `ensures` clauses, and let the prover do the rest for you, automatically.

diff --git a/v4.4.0/StyleGuide/Style-Guide.md b/v4.4.0/StyleGuide/Style-Guide.md
@@ -1,4 +1,8 @@
-<font size="+4"><p style="text-align: center;">Dafny Style Guide</p></font>
+---
+title: Dafny Style Guide
+---
+
+# Dafny Style Guide
 
 * toc
 {:toc}

diff --git a/v4.4.0/VerificationOptimization/VerificationOptimization.md b/v4.4.0/VerificationOptimization/VerificationOptimization.md
@@ -1,3 +1,7 @@
+---
+title: Verification Optimization
+---
+
 # Overview
 
 Dafny verifies your program using a type of theorem prover known as a Satisfiability Modulo Theories (SMT) solver. More specifically, it uses the [Z3](https://github.com/Z3Prover/z3) solver. In many cases, it's possible to state only the final properties you want your program to have, with annotations such as `requires` and `ensures` clauses, and let the prover do the rest for you, automatically.