1#!/bin/csh -f 2 3set a2ml = ${ACL2_HOL_LISP}/a2ml 4 5if ( ($#argv != 2) && ($#argv != 3)) then 6 echo "Usage: $0 infile outfile [infile_dir]" 7 exit 1 8endif 9 10set tmpfile = /tmp/workxxx 11set infile = $argv[1] 12set outfile = $argv[2] 13if ( ($#argv == 3)) then 14 set infile_dir = $argv[3] 15else 16 set infile_dir = "" 17endif 18 19rm -f $tmpfile 20echo "(include-book " '"'"${a2ml}"'")' > $tmpfile 21echo "(a2ml "'"'"$infile"'" "'"$outfile"'" "'"$infile_dir"'")' >> $tmpfile 22echo "(value :q) (quit)" >> $tmpfile 23${ACL2} < $tmpfile 24