[m-rev.] diff: bootcheck --write-out-profile-data

[Zoltan Somogyi]

tools/bootcheck:
	Add a new option, --write-out-profile-data, which causes bootcheck not
	to turn off the writing out of profiling data files, either during the
	building of the stages 2 and 3 or during the tests.

Zoltan.

cvs diff: Diffing .
Index: bootcheck
===================================================================
RCS file: /home/mercury1/repository/mercury/tools/bootcheck,v
retrieving revision 1.119
diff -u -b -r1.119 bootcheck
--- bootcheck	2001/05/31 06:00:24	1.119
+++ bootcheck	2001/07/16 01:15:59
@@ -80,6 +80,12 @@
 	--compile-times
 		Report information about compilation times in the stage 2
 		library and compiler directories.
+	--write-out-profile-data
+		When doing bootcheck in a deep profiling grade, enable the
+		writing out of profile data files. Since all compilations save
+		their profiling data in the same file, this is useful mainly to
+		check that we don't get fatal errors during the writing out
+		process.
 	--type-stats TYPE_STATS_FILE_NAME
 		Collect statistics about the builtin operations (unify, index
 		and compare) performed on various types. The argument of this
@@ -128,6 +134,7 @@
 	use_subdirs=${MMAKE_USE_SUBDIRS=no}
 fi
 compile_times=false
+write_out_profile_data=false
 type_stats=""
 
 if test -d .KEEP_OBJS
@@ -233,6 +240,9 @@
 	--no-compile-times)
 		compile_times=false ;;
 
+	--write-out-profile-data)
+		write_out_profile_data=true ;;
+
 	--type-stats)
 		type_stats="$2"; shift ;;
 
@@ -370,13 +380,18 @@
 		fi
 	fi
 
-	# Turn off the writing out of deep profiling files, since Deep.data
-	# will be overwritten many times in each directory, and thus the time
-	# spent writing them out is wasted. If deep profiling debugging is
-	# enabled, this also avoids the writing of *huge* amounts of stuff
-	# on stderr.
+	if $write_out_profile_data
+	then
+		true
+	else
+		# Turn off the writing out of deep profiling files, since
+		# Deep.data will be overwritten many times in each directory,
+		# and thus the time spent writing them out is wasted. If deep
+		# profiling debugging is enabled, this also avoids the writing
+		# of *huge* amounts of stuff on stderr.
 	MERCURY_OPTIONS="$MERCURY_OPTIONS -s"
 	export MERCURY_OPTIONS
+	fi
 
 	MERCURY_COMPILER=$root/compiler/mercury_compile
 	export MERCURY_COMPILER
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------