remove second title

leanprover-community · Jun 23, 2024 · b066ecd · b066ecd
1 parent 2d67629
commit b066ecd
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -226,8 +226,8 @@ jobs:
           if [ "$(printf '%s' "${ddiff}" | wc -l)" -gt 12 ]
           then
             ddiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "Report" "${ddiff}")"
-          else
-            ddiff="$(printf '%s\n\n%s\n' "${title}" "${ddiff}")"
+          #else
+          #  ddiff="$(printf '%s\n\n%s\n' "${title}" "${ddiff}")"
           fi
 
           echo "Message: ${ddiff}"

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -233,8 +233,8 @@ jobs:
           if [ "$(printf '%s' "${ddiff}" | wc -l)" -gt 12 ]
           then
             ddiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "Report" "${ddiff}")"
-          else
-            ddiff="$(printf '%s\n\n%s\n' "${title}" "${ddiff}")"
+          #else
+          #  ddiff="$(printf '%s\n\n%s\n' "${title}" "${ddiff}")"
           fi
 
           echo "Message: ${ddiff}"

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -211,8 +211,8 @@ jobs:
           if [ "$(printf '%s' "${ddiff}" | wc -l)" -gt 12 ]
           then
             ddiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "Report" "${ddiff}")"
-          else
-            ddiff="$(printf '%s\n\n%s\n' "${title}" "${ddiff}")"
+          #else
+          #  ddiff="$(printf '%s\n\n%s\n' "${title}" "${ddiff}")"
           fi
 
           echo "Message: ${ddiff}"

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -230,8 +230,8 @@ jobs:
           if [ "$(printf '%s' "${ddiff}" | wc -l)" -gt 12 ]
           then
             ddiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "Report" "${ddiff}")"
-          else
-            ddiff="$(printf '%s\n\n%s\n' "${title}" "${ddiff}")"
+          #else
+          #  ddiff="$(printf '%s\n\n%s\n' "${title}" "${ddiff}")"
           fi
 
           echo "Message: ${ddiff}"