fix: Backport additional Jekyll changes (#39)

fabiomadge · web-flow · commit 73da6bd9ad0d · 2024-02-21T17:43:41.000+01:00
Same as dafny-lang/dafny#5014
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.
