[Matita] Matita make install
tassi at cs.unibo.it
Thu Sep 16 18:02:58 CEST 2010
On Thu, Sep 16, 2010 at 11:38:37AM -0400, roconnor at theorem.ca wrote:
> I have a question about how Matita's make install works.
> in matita/Makefile we have the line:
> WHERE = $(DESTDIR)/$(RT_BASE_DIR)
> WHERE is the directory where matita installs things, but as you can
> see, it is alway a subdirectory of DESTDIR which is the place that
> matita was unpacked. The install never puts anything into designated
> system place.
> I wonder if this is an error, or is there some aspect of the install
> that I'm misunderstanding?
DESTDIR is a variable meant to be set by package-builders for linux
distributions to have the software installed in a place different from
the one it has been configured to be actually installed.
Example: if DESTDIR is empty, the application is installed in /usr/,
while when the debian package is built, DESTDIR is set to debian/tmp, so
that all files end up in a temporary directory.
It's is a pretty standard variable, Makefiles generated by autotools,
CMake, etc.. follow this convention (and the ugly, hand made, matita
Makefiles should do too).
More information about the Matita