diff options
| author | Gaëtan Gilbert | 2017-09-11 13:54:58 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-09-11 13:54:58 +0200 |
| commit | 3a849429dac4da9acf8538ee4a888ca53b4811cb (patch) | |
| tree | 7c6527726b39599ba0abaf9f636033a1d144e73f /API/API.mli | |
| parent | 4882288ba34ad0c47f950e733ae353a1b881df77 (diff) | |
Remove unneeded fix for BZ#1715
It hasn't been necessary since
6aad0d9cd2104b5343ed7c831a4ad0bbe34007cb introduced $(INSTALLLIB)
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions