[m-rev.] diff: test_mercury: enable deep profiler for source distribution

[Simon Taylor]

Estimated hours taken: 0.25

tools/test_mercury:
	Commit an old change of Fergus's to enable the deep profiler
	on the host building the source distribution.

Index: test_mercury
===================================================================
RCS file: /home/mercury1/repository/mercury/tools/test_mercury,v
retrieving revision 1.167
diff -u -u -r1.167 test_mercury
--- test_mercury	7 Nov 2001 06:21:28 -0000	1.167
+++ test_mercury	7 Nov 2001 16:45:35 -0000
@@ -378,6 +378,14 @@
 		CONFIG_OPTS="" ;;
 esac
 
+
+	# The deep profiler needs to be included in the source distribution.
+case $HOST in $ROTD_HOST)
+	CONFIG_OPTS="$CONFIG_OPTS \
+	    --enable-deep-profiler=/home/mercury/public/installed_w3/cgi-bin"
+	;;
+esac
+
 #-----------------------------------------------------------------------------#
 
 # Sometimes, bootstrapping problems mean that we need to install
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------