From ac9e02424c38dfb00e9c2eda83c14bbb8d3ff0d3 Mon Sep 17 00:00:00 2001 From: Dimitri Merejkowsky Date: Sat, 8 Dec 2018 12:24:44 +0100 Subject: [PATCH] Remove useless script --- sessions/release.sh | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100755 sessions/release.sh diff --git a/sessions/release.sh b/sessions/release.sh deleted file mode 100755 index c3b966c..0000000 --- a/sessions/release.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/zsh - -set -e - -if [[ -z $1 ]]; then - echo "Usage: build.sh NUMBER" - exit 1 -fi - - -darkslide --linenos=no "${1}.md" --embed --destination "${1}.html" -prince "${1}.html" -o "${1}.pdf"