[m-dev.] there is no --strip=false option to ./configure

[Terrence Brannon]

in order to avoid my error when -s is used in the final link, I wanted
to set a configure option, but I guess I should just edit ml.in. 

I would rather have a configuration option.

-- 
Carter's Compass: I know I'm on the right track when 
by deleting something I'm adding functionality.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------