From 7f07eeff9f43b359f7b1b0e65689021bf68c19d6 Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Mon, 11 Mar 2019 14:57:18 -0700 Subject: Fix typo in Makefile. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 580a35a..f2e4d61 100644 --- a/Makefile +++ b/Makefile @@ -241,7 +241,7 @@ generated_definitions/hol4/$(ARCH)/riscvScript.sml: generated_definitions/hol4/$ generated_definitions/lem/$(ARCH)/riscv_types.lem \ generated_definitions/lem/$(ARCH)/riscv.lem -$(addprefix generated_definitions/hol4/$(ARCH),riscvTheory.uo riscvTheory.ui): generated_definitions/hol4/$(ARCH)/Holmakefile generated_definitions/hol4/$(ARCH)/riscvScript.sml +$(addprefix generated_definitions/hol4/$(ARCH)/,riscvTheory.uo riscvTheory.ui): generated_definitions/hol4/$(ARCH)/Holmakefile generated_definitions/hol4/$(ARCH)/riscvScript.sml ifeq ($(wildcard $(LEM_DIR)/hol-lib),) $(error Lem directory not found. Please set the LEM_DIR environment variable) endif -- cgit v1.1