diff options
| author |  Nicolas Braud-Santoni <nicolas@braud-santoni.eu> | 2016-07-23 16:26:21 -0400 |
|---|---|---|
| committer | Nicolas Braud-Santoni <nicolas@braud-santoni.eu> | 2016-07-23 16:44:14 -0400 |
| commit | f2abc870b150ff1296576c7028941e57ee1c27ab (patch) | |
| tree | 736cf6e21d1fd4ee6d9319009dd6a92aba99b0bf /theory.mli | |
| parent | a3a7c528787411373bb857af4b51f3003f9fcc2b (diff) | |
debian/rules: Do not fail on non-installed files
We do not install, on purpose, .glob and .v files.
Diffstat (limited to 'theory.mli')
0 files changed, 0 insertions, 0 deletions