#
set echo
set time = 1
C
C --- dummy script, doing nothing
C
