diff --git a/regen b/regen new file mode 100755 index 0000000000..0d894688cc --- /dev/null +++ b/regen @@ -0,0 +1,18 @@ +#!/bin/sh +# +# regenerates the file given as command line argument by running config.status +# (the file is supposed to be generated by configure script) +# +# Version: $Id$ +# Author: VZ +################################################################################ + +if test "x$1" = "x"; then + echo "Usage: $0 file_to_regenerate" >&2 + exit 1 +fi + +export CONFIG_FILES=$1 +export CONFIG_HEADERS= +./config.status +exit $?