From cdacf7b0ac76e35b52d6dd6d70cde683858c5900 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 9 Jun 2023 10:32:03 -0600 Subject: [PATCH] Change `_pdf` to `.pdf`. --- DocGen4/Process/NameExt.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Process/NameExt.lean b/DocGen4/Process/NameExt.lean index d495cc5..7353b1a 100644 --- a/DocGen4/Process/NameExt.lean +++ b/DocGen4/Process/NameExt.lean @@ -37,7 +37,7 @@ def cmp (n₁ n₂ : NameExt) : Ordering := def getString! : NameExt → String | ⟨str _ s, .html⟩ => s - | ⟨str _ s, .pdf⟩ => s ++ "_pdf" + | ⟨str _ s, .pdf⟩ => s ++ ".pdf" | _ => unreachable! end NameExt