From 897bb1ec68d2fe03c8d6d3c90e05555498912273 Mon Sep 17 00:00:00 2001 From: hondet <gabrielhondet@gmail.com> Date: Sun, 7 Feb 2021 18:30:06 +0100 Subject: [PATCH] Install only encoding --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 950c22d..5c656bc 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ LP = lambdapi -LP_SRC != find encodings prelude -type f -name "*.lp" +LP_SRC != find encodings -type f -name "*.lp" LP_OBJ = ${LP_SRC:S/.lp$/.lpo/} .SUFFIXES: .lpo .lp -- GitLab