hugs makefiles and Debian

Ross Paterson ross@soi.city.ac.uk
Tue, 4 Feb 2003 17:43:40 +0000


On Tue, Feb 04, 2003 at 11:09:46AM -0500, Isaac Jones wrote:
> [...]
> Is there a way you or I can alter the build system so ffihugs looks at
> the right place at the right time? (It looks at $DESTDIR during
> installation and in the correct place afterward).

I'd suggest

	cd src && HUGSDIR=$(rootdir)/usr/share/hugs98 $(MAKE) DESTDIR=$(rootdir) install

The environment variable HUGSDIR is used by hugs (and ffihugs) to
find files.

Also, an alternative to changing the makefiles might be

	hugsdir=/usr/share/hugs98 configure --prefix=$(rootdir)/usr/share/hugs98 

BTW, Hugs will install object files under that directory (it doesn't
separate share and lib properly, and that's not trivial to fix) so
you probably want lib.