From 73da6bd9ad0d24c632d7ba47858cd09e1712fc15 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 21 Feb 2024 17:43:41 +0100 Subject: [PATCH] fix: Backport additional Jekyll changes (#39) Same as https://github.com/dafny-lang/dafny/pull/5014 --- latest/StyleGuide/Style-Guide.md | 6 +++++- latest/VerificationOptimization/VerificationOptimization.md | 4 ++++ v3.10.0/StyleGuide/Style-Guide.md | 6 +++++- v3.11.0/StyleGuide/Style-Guide.md | 6 +++++- v3.12.0/StyleGuide/Style-Guide.md | 6 +++++- v3.13.1/StyleGuide/Style-Guide.md | 6 +++++- v3.9.0/StyleGuide/Style-Guide.md | 6 +++++- v3.9.1/StyleGuide/Style-Guide.md | 6 +++++- v4.0.0/StyleGuide/Style-Guide.md | 6 +++++- v4.1.0/StyleGuide/Style-Guide.md | 6 +++++- v4.1.0/VerificationOptimization/VerificationOptimization.md | 4 ++++ v4.2.0/StyleGuide/Style-Guide.md | 6 +++++- v4.2.0/VerificationOptimization/VerificationOptimization.md | 4 ++++ v4.3.0/StyleGuide/Style-Guide.md | 6 +++++- v4.3.0/VerificationOptimization/VerificationOptimization.md | 4 ++++ v4.4.0/StyleGuide/Style-Guide.md | 6 +++++- v4.4.0/VerificationOptimization/VerificationOptimization.md | 4 ++++ 17 files changed, 80 insertions(+), 12 deletions(-) diff --git a/latest/StyleGuide/Style-Guide.md b/latest/StyleGuide/Style-Guide.md index bb6d049..e80f507 100644 --- a/latest/StyleGuide/Style-Guide.md +++ b/latest/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +title: Dafny Style Guide +--- + +# Dafny Style Guide * toc {:toc} diff --git a/latest/VerificationOptimization/VerificationOptimization.md b/latest/VerificationOptimization/VerificationOptimization.md index 8b9adf9..d7052b7 100644 --- 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 index bb6d049..e80f507 100644 --- a/v3.10.0/StyleGuide/Style-Guide.md +++ b/v3.10.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index bb6d049..e80f507 100644 --- a/v3.11.0/StyleGuide/Style-Guide.md +++ b/v3.11.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index bb6d049..e80f507 100644 --- a/v3.12.0/StyleGuide/Style-Guide.md +++ b/v3.12.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index bb6d049..e80f507 100644 --- a/v3.13.1/StyleGuide/Style-Guide.md +++ b/v3.13.1/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index bb6d049..e80f507 100644 --- a/v3.9.0/StyleGuide/Style-Guide.md +++ b/v3.9.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index bb6d049..e80f507 100644 --- a/v3.9.1/StyleGuide/Style-Guide.md +++ b/v3.9.1/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index bb6d049..e80f507 100644 --- a/v4.0.0/StyleGuide/Style-Guide.md +++ b/v4.0.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index bb6d049..e80f507 100644 --- a/v4.1.0/StyleGuide/Style-Guide.md +++ b/v4.1.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index a5f452e..c65f43a 100644 --- 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 index bb6d049..e80f507 100644 --- a/v4.2.0/StyleGuide/Style-Guide.md +++ b/v4.2.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index 8b9adf9..d7052b7 100644 --- 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 index bb6d049..e80f507 100644 --- a/v4.3.0/StyleGuide/Style-Guide.md +++ b/v4.3.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index 8b9adf9..d7052b7 100644 --- 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 index bb6d049..e80f507 100644 --- a/v4.4.0/StyleGuide/Style-Guide.md +++ b/v4.4.0/StyleGuide/Style-Guide.md @@ -1,4 +1,8 @@ -

Dafny Style Guide

 +--- +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 index 8b9adf9..d7052b7 100644 --- 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.