From e915c63a97bb0d49ba1eddb1579c07839c26e980 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sun, 17 Feb 2019 17:08:35 -0500 Subject: Don’t install .cm(a|x|xa) files MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- debian/not-installed | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 debian/not-installed diff --git a/debian/not-installed b/debian/not-installed new file mode 100644 index 0000000..0f62dd4 --- /dev/null +++ b/debian/not-installed @@ -0,0 +1,3 @@ +usr/lib/coq/user-contrib/AAC_tactics/aac_plugin.cma +usr/lib/coq/user-contrib/AAC_tactics/aac_plugin.cmx +usr/lib/coq/user-contrib/AAC_tactics/aac_plugin.cmxa -- cgit v1.2.3