refactor: don't generate empty block

Seasawher · Apr 2, 2024 · 059dc77 · 059dc77
1 parent daad84f
commit 059dc77
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Mdgen/ConvertToMd.lean b/Mdgen/ConvertToMd.lean
@@ -25,7 +25,9 @@ private def buildBlocks (lines : List String) : List Block := Id.run do
         panic!
           "Nested lean commentary sections not allowed in:\n" ++
           s!" line {i+1}: {line}"
-      blocks ++= [{content := content.trim, toCodeBlock := toCodeBlock}]
+
+      if content != "" then
+        blocks ++= [{content := content.trim, toCodeBlock := toCodeBlock}]
       toCodeBlock := ! toCodeBlock
       content := line ++ "\n"