fix incorrect variable in makefile preventing install

This commit is contained in:
Arnaud Bailly 2019-09-22 22:43:08 +02:00
parent 2f8daa7cf2
commit c80bfc0ed7

View File

@ -2,7 +2,7 @@
MAJOR=0
MINOR=0
PATCH=0
IDRIS2_VERSION="$MAJOR.$MINOR.$PATCH"
IDRIS2_VERSION=${MAJOR}.${MINOR}.${PATCH}
PREFIX ?= ${HOME}/.idris2
IDRIS_VERSION := $(shell idris --version)
VALID_IDRIS_VERSION_REGEXP = "1.3.2.*"