Merge pull request #1775 from bhundven/bootstrap_mixed_indent

Fix mixed indent in bootstrap
This commit is contained in:
Bryan Hundven 2022-06-29 13:01:52 -07:00 committed by GitHub
commit 8e572114c2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -1,4 +1,5 @@
#!/usr/bin/env bash
# vi: ts=4:sw=4:et
if [ "${BASH_VERSINFO[0]}" -lt 4 ]; then
echo "Your BASH shell version (${BASH_VERSION}) is too old." >&2
@ -470,15 +471,15 @@ sort_versions()
#debug "${v} vs ${vx} :: `cmp_versions ${v} ${vx}`"
case `cmp_versions ${v} ${vx}` in
1)
next_remains+=" ${vx}"
;;
next_remains+=" ${vx}"
;;
0)
;;
;;
-1)
found=no
#debug "Bad: earlier than ${vx}"
break
;;
found=no
#debug "Bad: earlier than ${vx}"
break
;;
esac
done
if [ "${found}" = "yes" ]; then
@ -823,7 +824,7 @@ msg "*** Gathering the list of data files to install"
continue
fi
echo " \\"
echo -n " ${f}"
echo -en "\t${f}"
seen_files[${f}]=y
done
} > verbatim-data.mk