ID: 4cce1b7bbdc2347ecc326fd0c3dde67561b2a178
31 lines
—
587B —
View raw
| SHELL = /bin/bash
REPOSITORY = https://github.com/idris-lang/Idris-dev.git
check_env_vars:
ifdef OUTPUT_PATH
OUTPUT_PATH := ${OUTPUT_PATH}/idris-lang
else
$(error OUTPUT_PATH is undefined)
endif
venv:
python3 -m venv venv
repository:
git clone ${REPOSITORY} repository
v1.3.2 v1.3.3 v1.3.4: check_env_vars venv repository
mkdir --parents "${OUTPUT_PATH}"
source venv/bin/activate
cd repository
git checkout tags/$@
pip install sphinx sphinx-rtd-theme
cd docs
make dirhtml
cp --recursive _build/dirhtml "${OUTPUT_PATH}/$@"
.ONESHELL:
.SUFFIXES:
.PHONY:
.DELETE_ON_ERROR:
|