[Matita] Matita make install

[Enrico Tassi]

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).

Cheers.
-- 
Enrico Tassi