diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2019-02-17 17:08:35 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2019-02-17 17:08:35 -0500 |
| commit | e915c63a97bb0d49ba1eddb1579c07839c26e980 (patch) | |
| tree | d6140f271bf666672c247a3666854842a9ab582d | |
| parent | 47393169db58d0556481d9a13007f047a5c6fdaa (diff) | |
Don’t install .cm(a|x|xa) files
| -rw-r--r-- | debian/not-installed | 3 |
1 files changed, 3 insertions, 0 deletions
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 |