Improve behaviour if md5sum is not installed.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
This commit is contained in:
parent
04377e6727
commit
c3ecbc8a24
6
install
6
install
|
@ -117,14 +117,16 @@ check_isa_dof_patch() {
|
|||
echo "* Check availabilty of Isabelle/DOF patch:"
|
||||
src="patches/thy_output.ML"
|
||||
dst="$ISABELLE_HOME/src/Pure/Thy/thy_output.ML"
|
||||
if [[ $(md5sum "$src" | cut -d' ' -f1) = $(md5sum "$dst" | cut -d' ' -f1) ]]; then
|
||||
|
||||
if command -v md5sum > /dev/null 2>&1 && [[ $(md5sum "$src" | cut -d' ' -f1) = $(md5sum "$dst" | cut -d' ' -f1) ]]; then
|
||||
echo " Success: latest Isabelle/DOF patch already applied"
|
||||
if isabelle process -e 'Thy_Output.set_meta_args_parser' &> /dev/null ; then
|
||||
true
|
||||
else
|
||||
echo " Success: Warning: Isabelle/HOL needs to be rebuild to activate patch."
|
||||
echo " Warning: Isabelle/HOL needs to be rebuild to activate patch."
|
||||
fi
|
||||
else
|
||||
command -v md5sum >/dev/null 2>&1 || echo " Warning: md5sum not available, cannot check if patch is already applied."
|
||||
echo " Warning: Isabelle/DOF patch is not available or outdated."
|
||||
echo " Trying to patch system ...."
|
||||
if (cp $dst $dst.backup-by-isadof-installer && cp -f $src $dst) &> /dev/null; then
|
||||
|
|
Loading…
Reference in New Issue