Removed output file argument to highlight.sh as part of #342
This commit is contained in:
parent
3e1b75f30c
commit
cfab4e778f
2 changed files with 9 additions and 4 deletions
4
Makefile
4
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/<filename> to out/<filepath>)
|
||||
./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
|
||||
|
|
|
@ -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'
|
||||
|
|
Loading…
Reference in a new issue