diff --git a/Makefile b/Makefile index 2bdb8ec0..cd14dfbf 100644 --- a/Makefile +++ b/Makefile @@ -40,10 +40,10 @@ $$(out) : out = $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$( $$(out) : $$(in) | out/ @echo "Processing $$(subst ./,,$$(in))" ifeq (,$$(findstring courses/,$$(in))) - ./highlight.sh $$(in) $$(out) + ./highlight.sh $$(in) else # Fix links to the file itself (out/ to out/) - ./highlight.sh $$(in) $$(out) --include-path $(realpath src) --include-path $$(realpath $$(dir $$(in))) + ./highlight.sh $$(in) --include-path $(realpath src) --include-path $$(realpath $$(dir $$(in))) @sed -i 's|out/$$(notdir $$(out))|$$(subst ./,,$$(out))|g' $$(out) endif endef diff --git a/highlight.sh b/highlight.sh index 9080a2aa..c8abca36 100755 --- a/highlight.sh +++ b/highlight.sh @@ -5,9 +5,14 @@ AGDA_STDLIB_SED=".agda-stdlib.sed" SRC="$1" shift -OUT="$1" +function out_path { + OUT="$1" + OUT=$(eval "echo \"$OUT\" | sed -e \"s|/src/|/out/|; s|/courses/|/out/|; s|\.lagda\.md|\.md|;\"") + echo "$OUT" +} + +OUT="$(out_path $SRC)" OUT_DIR="$(dirname $OUT)" -shift # Extract the module name from the Agda file # NOTE: this fails if there is more than a single space after 'module'