From 85b9126c4321f07e0d96a4f544d0ff21c87e42bd Mon Sep 17 00:00:00 2001
From: Michael Hanus <mh@informatik.uni-kiel.de>
Date: Mon, 22 Jan 2018 12:09:25 +0100
Subject: [PATCH] Makefile: deprecated parameter -cpm removed

---
 resource_files/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/resource_files/Makefile b/resource_files/Makefile
index d72ebe9..456346a 100644
--- a/resource_files/Makefile
+++ b/resource_files/Makefile
@@ -49,7 +49,7 @@ run:
 .PHONY: deploy
 deploy:
 	mkdir -p $(WEBSERVERDIR)
-	$(CPM) exec $(CURRYBIN)/curry makecgi -cpm -standalone -m main -o $(WEBSERVERDIR)/spicey.cgi Main.curry
+	$(CPM) exec $(CURRYBIN)/curry makecgi -standalone -m main -o $(WEBSERVERDIR)/spicey.cgi Main.curry
 	# copy other files (style sheets, images,...)
 	cp -r public/* $(WEBSERVERDIR)
 	chmod -R go+rX $(WEBSERVERDIR)
-- 
GitLab