#! /bin/sh
-# Copyright (C) 2001-2012 Free Software Foundation, Inc.
+# Copyright (C) 2001-2013 Free Software Foundation, Inc.
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
./configure
-EXEEXT=.foo $MAKE -e print > stdout
-cat stdout
+run_make -O EXEEXT=.foo print
grep '1BEG: maude.foo mt.foo :END1' stdout
grep '2BEG: maude.static.foo :END2' stdout
./configure revert=yes
-EXEEXT=.foo $MAKE -e print > stdout
-cat stdout
+run_make -O EXEEXT=.foo print
grep '1BEG: maude.foo :END1' stdout
grep '2BEG: maude.static.foo :END2' stdout