mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-18 07:15:19 +00:00
d3aa462819
Estimated hours taken: 0.5
scripts/Mmake.rules
scripts/Mmake.vars.in
Add suffixes, rules and options for .opt and .optdate.
scripts/mercury_update_interface.in
Work-around for a problem with parallel gmake. mc --make-interface
was being run twice in a row on the same module. The first call
mercury_update_interface moves module.int.tmp to module.int,
then the second can't find module.int.tmp. The work-around is to
ignore the exit status of the mv.
55 lines
1.3 KiB
Bash
55 lines
1.3 KiB
Bash
#! /bin/sh
|
|
# @configure_input@
|
|
#---------------------------------------------------------------------------#
|
|
# Copyright (C) 1995 University of Melbourne.
|
|
# This file may only be copied under the terms of the GNU General
|
|
# Public License - see the file COPYING in the Mercury distribution.
|
|
#---------------------------------------------------------------------------#
|
|
#
|
|
# MERCURY_UPDATE_INTERFACE
|
|
#
|
|
# usage:
|
|
# mercury_update_interface [-v] filename
|
|
#
|
|
# Moves `filename.tmp' to `filename', but only if necessary:
|
|
# if they are identical, then `filename.tmp' is simply removed,
|
|
# and the time-stamp is left unaltered.
|
|
#
|
|
# If the `-v' (verbose) option is specified, then appropriate progress messages
|
|
# will be printed.
|
|
#
|
|
# Enviroment variables: none.
|
|
|
|
PATH=/bin:/usr/bin
|
|
|
|
verbose=false
|
|
|
|
if [ $# -ge 1 ] && [ "$1" = "-v" ]; then
|
|
verbose=true
|
|
shift
|
|
fi
|
|
|
|
if [ $# -ne 1 ]; then
|
|
echo "Usage: `basename $0` filename" 1>&2
|
|
exit 1
|
|
fi
|
|
|
|
filename="$1"
|
|
|
|
if [ ! -f "$filename" ]
|
|
then
|
|
$verbose && echo "creating \`$filename'." 1>&2
|
|
mv -f "$filename.tmp" "$filename"
|
|
# Work-around for a parallel gmake problem
|
|
exit 0
|
|
elif cmp -s "$filename.tmp" "$filename"
|
|
then
|
|
$verbose && echo "\`$filename' has not changed." 1>&2
|
|
rm -f "$filename.tmp"
|
|
else
|
|
$verbose && echo "\`$filename' has changed." 1>&2
|
|
mv -f "$filename.tmp" "$filename"
|
|
# Work-around for a parallel gmake problem
|
|
exit 0
|
|
fi
|