From: Stefano Zacchiroli Date: Sun, 20 Jan 2002 14:46:32 +0000 (+0000) Subject: Added "-destdir" argument to "ocamlfind install" in "install:" X-Git-Tag: mlminidom_0_2_2~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=09aa799947c84148221af82e94e911adea8fd1e6;hp=09aa799947c84148221af82e94e911adea8fd1e6;p=helm.git Added "-destdir" argument to "ocamlfind install" in "install:" target of Makefile.in, ease creation of debian package and non standard installation. ---