1#!/usr/bin/env bash 2# 3# Author: Gerwin Klein 4# 5# make a copy of IMP with isaverbatimwrite lines in thy files removed 6 7## diagnostics 8 9function fail() 10{ 11 echo "$1" >&2 12 exit 2 13} 14 15## main 16 17EXPORT=IMP 18 19rm -rf "$EXPORT" 20 21# make directories 22 23DIRS=$(find . -type d) 24for D in $DIRS; do 25 mkdir -p "$EXPORT/$D" || fail "could not create directory $EXPORT/$D" 26done 27 28# filter thy files 29 30FILES=$(find . -name "*.thy") 31for F in $FILES; do 32 grep -v isaverbatimwrite "$F" > "$EXPORT/$F" 33done 34 35# copy rest 36 37cp ROOT.ML "$EXPORT" 38cp -r document "$EXPORT" 39 40# tar and clean up 41tar cvzf "$EXPORT.tar.gz" "$EXPORT" 42rm -r "$EXPORT" 43