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