From 70bcdeec9a18c2b9035e5b87aba9939d9d1ed805 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 20 May 2019 16:11:55 +0100 Subject: [PATCH] Fix #260 --- Makefile | 7 ++++++- README.md | 2 +- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 07fff5d5..753ddf8a 100644 --- a/Makefile +++ b/Makefile @@ -4,6 +4,11 @@ markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,.md,$(agda)))) PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST)))) AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/ +ifeq ($(AGDA_STDLIB_VERSION),) +AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/ +else +AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/v$(AGDA_STDLIB_VERSION)/ +endif # Build PLFA and test hyperlinks test: build @@ -53,7 +58,7 @@ server-stop: # Build website using jekyll -build: AGDA2HTML_FLAGS += --link-to-agda-stdlib +build: AGDA2HTML_FLAGS += --link-to-agda-stdlib=$(AGDA_STDLIB_URL) build: $(markdown) ruby -S bundle exec jekyll build diff --git a/README.md b/README.md index 85d2ac12..42ef5f07 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ permalink: /GettingStarted/ [![Build Status](https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev)](https://travis-ci.org/plfa/plfa.github.io) [![Agda](https://img.shields.io/badge/agda-2.5.4.2-blue.svg)](https://github.com/agda/agda/releases/tag/v2.5.4.2) [![agda-stdlib](https://img.shields.io/badge/agda--stdlib-0.17-blue.svg)](https://github.com/agda/agda-stdlib/releases/tag/v0.17) -[![agda2html](https://img.shields.io/badge/agda2html-0.2.3.0-blue.svg)](https://github.com/wenkokke/agda2html/releases/tag/v0.2.3.0) +[![agda2html](https://img.shields.io/badge/agda2html-0.2.4.0-blue.svg)](https://github.com/wenkokke/agda2html/releases/tag/v0.2.4.0) # Getting Started with PLFA