From 5cbf17b425de73dd58c25f4b3c371337494000a8 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 17 Nov 2020 14:23:41 -0800 Subject: [PATCH] Leave Markdown files out of distribution packages (#971) --- .github/ci.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/ci.sh b/.github/ci.sh index dd237501..13700032 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -145,7 +145,7 @@ bundle_files() { mkdir -p $doc cp -R examples/ $doc/examples/ rm -rf $doc/examples/cryptol-specs - cp docs/*md docs/*pdf $doc + cp docs/*pdf $doc # Copy the two interesting examples over cp docs/ProgrammingCryptol/{aes/AES,enigma/Enigma}.cry $doc/examples/