#!/bin/bash

usage(){
echo "usage: $0 CHECKED_DVIFILE GOOD_DVIFILE"
exit 1
}

[ -z $1 ] && usage
[ -z $2 ] && usage

checked_file=$1
result_file=$2

[ ! -f "$result_file" ] && { echo "no file $result_file" ; exit 1 ; }
[ ! -f "$checked_file" ] && { echo "no file $checked_file" ; exit 1 ; }

if ! dvitype $checked_file | sed -e "1d
/^'.*$/ d" > $checked_file.dvitype; then
exit 1
fi

dvitype $result_file | sed -e "1d
/^'.*$/ d" | diff -u - $checked_file.dvitype 
ret=$?

[ $ret = 0 ] && rm -f $checked_file.dvitype

exit $ret