#! /bin/csh -f
# Last edited on 1999-03-20 11:21:58 by stolfi

set usage = "$0 NAME"

if ( $#argv != 1 ) then
  echo "usage: ${usage}"; exit 1
endif

set name = "$1"; shift

test-f ${name} 1.0
test-f ${name} 1.5
test-f ${name} 2.0
test-f ${name} 3.0
test-f ${name} 4.0
test-f ${name} 5.0
test-h ${name}
test-m ${name}