raw output with flag

leanprover-community · Aug 2, 2024 · 44af846 · 44af846
1 parent 957c8fc
commit 44af846
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/monthly_summary.sh b/monthly_summary.sh
@@ -110,7 +110,7 @@ fi
 printf -- $'---\n'
 
 rm -rf found_by_gh.txt found_by_git.txt
-} | if [ -n "${raw}" ]; then cat; else  # extra .md formatting
+} | if [ "${raw}" == "raw" ]; then cat; else  # extra .md formatting
   sed '
     / [0-9]* PRs$/{
       s=^=</details><details><summary>\n=