Merge branch 'dev' of github.com:plfa/plfa.github.io into dev

2019-10-04 18:25:05 +01:00 · 2019-10-04 18:25:05 +01:00 · b066c247c1
commit b066c247c1
parent 4c5f4f6d93 d0597244e4
1 changed files with 14 additions and 0 deletions
--- a/exercise.sh
+++ b/exercise.sh
@ -0,0 +1,14 @@
+#!/bin/bash
+
+# Script to extract exercises from PLFA chapters, e.g., `src/plfa/part1/Naturals.lagda.md`.
+# Usage:
+#
+#   ./exercise.sh [SOURCE] [TARGET]
+
+SRC="$1"
+shift
+
+DST="$1"
+shift
+
+awk '/^#/{flag=0} /^#### Exercise/{flag=1} flag' "$SRC" > "$DST"