aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/vm_printers.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-11 13:54:58 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-11 13:54:58 +0200
commit3a849429dac4da9acf8538ee4a888ca53b4811cb (patch)
tree7c6527726b39599ba0abaf9f636033a1d144e73f /dev/vm_printers.ml
parent4882288ba34ad0c47f950e733ae353a1b881df77 (diff)
Remove unneeded fix for BZ#1715
It hasn't been necessary since 6aad0d9cd2104b5343ed7c831a4ad0bbe34007cb introduced $(INSTALLLIB)
Diffstat (limited to 'dev/vm_printers.ml')
0 files changed, 0 insertions, 0 deletions