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