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.