diff --git a/regen b/regen index 0d894688cc..b5ec049779 100755 --- a/regen +++ b/regen @@ -1,4 +1,4 @@ -#!/bin/sh +#!/bin/ksh # # regenerates the file given as command line argument by running config.status # (the file is supposed to be generated by configure script)