Skip to content

Commit

Permalink
foliadiff speedup: run 2 folialint's in parallel
Browse files Browse the repository at this point in the history
  • Loading branch information
kosloot committed Nov 20, 2024
1 parent b6ad074 commit 09a6e47
Showing 1 changed file with 13 additions and 12 deletions.
25 changes: 13 additions & 12 deletions src/foliadiff.sh
Original file line number Diff line number Diff line change
Expand Up @@ -40,20 +40,21 @@ if [ $# -ne 2 ]
exit 1
fi

run_lint(){
$exe --strip --KANON "$1" --output $2
if [ $? -ne 0 ]
then
echo "foliadiff.sh: $1 is INVALID FoLiA"
exit 1
fi
}

t1=/tmp/${1##*/}.s1
t2=/tmp/${2##*/}.s2
$exe --strip --KANON "$1" --output $t1
if [ $? -ne 0 ]
then
echo "foliadiff.sh: $1 is INVALID FoLiA"
exit 1
fi
$exe --strip --KANON "$2" --output $t2
if [ $? -ne 0 ]
then
echo "foliadiff.sh: $2 is INVALID FoLiA"
exit 1
fi

run_lint $1 $t1 &
run_lint $2 $t2 &
wait
diff $t1 $t2
if [ $? -ne 0 ]
then
Expand Down

0 comments on commit 09a6e47

Please sign in to comment.