|
#!/usr/bin/env bash
#
# Author: Gerwin Klein
#
# make a copy of IMP with isaverbatimwrite lines in thy files removed
## diagnostics
function fail()
{
echo "$1" >&2
exit 2
}
## main
EXPORT=IMP
rm -rf "$EXPORT"
# make directories
DIRS=$(find . -type d)
for D in $DIRS; do
mkdir -p "$EXPORT/$D" || fail "could not create directory $EXPORT/$D"
done
# filter thy files
FILES=$(find . -name "*.thy")
for F in $FILES; do
grep -v isaverbatimwrite "$F" > "$EXPORT/$F"
done
# copy rest
cp ROOT.ML "$EXPORT"
cp -r document "$EXPORT"
# tar and clean up
tar cvzf "$EXPORT.tar.gz" "$EXPORT"
rm -r "$EXPORT"
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
