equal
deleted
inserted
replaced
65 cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings |
65 cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings |
66 |
66 |
67 |
67 |
68 echo "Start test at `date`" > $LOG |
68 echo "Start test at `date`" > $LOG |
69 echo >> $LOG |
69 echo >> $LOG |
70 echo "begin cvs update" >> $LOG |
|
71 |
70 |
72 # cvs update to newest version |
|
73 cd $DOCDIR || fail "could not cd to $DOCDIR" |
71 cd $DOCDIR || fail "could not cd to $DOCDIR" |
74 cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update." |
|
75 |
|
76 echo "end cvs update" >> $LOG |
|
77 echo >> $LOG |
|
78 |
72 |
79 # run test |
73 # run test |
80 FAIL=""; |
74 FAIL=""; |
81 |
75 |
82 cd $DOCDIR |
76 cd $DOCDIR |