From 780f8cd77e166bfcce85423ed323d7d2618ff39a Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Wed, 10 Mar 2021 08:38:01 +0100
Subject: [PATCH] Fix regression test

---
 testcases/regression/Holmakefile | 22 +---------------------
 1 file changed, 1 insertion(+), 21 deletions(-)

diff --git a/testcases/regression/Holmakefile b/testcases/regression/Holmakefile
index 6c6bfcf5..edc96554 100644
--- a/testcases/regression/Holmakefile
+++ b/testcases/regression/Holmakefile
@@ -1,27 +1,7 @@
 INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra
 OPTIONS = QUIT_ON_FAILURE
 
-ifdef POLY
-HOLHEAP = heap
-EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
-all: $(HOLHEAP)
-
 THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
 TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
-all: $(TARGETS) $(HOLHEAP)
+all: $(TARGETS)
 .PHONY: all
-
-BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
-     alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib \
-     combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs \
-     listTheory llistTheory markerLib realTheory realLib RealArith\
-     optionTheory pairLib pairTheory pred_setTheory \
-     quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
-     sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
-     simpLib realTheory realLib RealArith
-
-DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
-
-$(HOLHEAP): $(DEPS)
-	$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
-endif
-- 
GitLab