From 8e708a30b165776ac8df65c5e5f440baff855f70 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Thu, 1 Jun 2017 17:11:42 +0200
Subject: test-suite/coq-makefile: we do not build byte file by default anymore

---
 test-suite/coq-makefile/plugin3/run.sh | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'test-suite/coq-makefile/plugin3')

diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index 24ef8c891b..c2d47166fe 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -17,12 +17,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
-- 
cgit v1.2.3