From f973e83978f7ae9faa4a68e725d7b0aca2017db3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me>
Date: Tue, 28 Apr 2020 18:31:56 +0000
Subject: [PATCH] isabelle-prepare.sh: use python script to fix iris
---
ulo/isabelle-prepare.sh | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/ulo/isabelle-prepare.sh b/ulo/isabelle-prepare.sh
index b1e787c..5f6e6fa 100755
--- a/ulo/isabelle-prepare.sh
+++ b/ulo/isabelle-prepare.sh
@@ -14,6 +14,9 @@ if [ ! $# -eq 1 ]; then
exit 1
fi
+script_dir=$(dirname "$0")
+cd "$script_dir"
+
directory="$1"
files=$(find "$directory" -name "*.xz")
@@ -22,12 +25,12 @@ for file in $files; do
# the filename of the extracted (uncompressed) file
rdf_file=$(echo "$file" | sed 's/\.xz//')
+ work_file=$(mktemp)
+
+ # uncompress, fix iris
+ xzcat "$file" | ./fix-rdf-file.py > "$work_file"
+ mv "$work_file" "$rdf_file"
- # uncompress, fix iris, compress again
- unxz "$file"
- sed -i 's/|/%7C/g' "$rdf_file"
- sed -i 's/\\/%5C/g' "$rdf_file"
- sed -i 's/ /%20/g' "$rdf_file"
- sed -i 's/\^/%5E/g' "$rdf_file"
+ # compress again
gzip "$rdf_file"
done
--
GitLab