2008-07-18 12:15:21 +02:00
|
|
|
#! /bin/bash
|
|
|
|
|
|
|
|
# lines 4 contains a timestamp...
|
|
|
|
differences="$(
|
2018-06-20 08:03:05 +02:00
|
|
|
diff -bU0 <(sed -e '/CONFIG_GCC_VERSION/ d' -e '/^# .* is not set$/p' -e '/^$\|^#/d' "$1" | sort) \
|
|
|
|
<(sed -e '/CONFIG_GCC_VERSION/ d' -e '/^# .* is not set$/p' -e '/^$\|^#/d' "$2" | sort) \
|
2008-07-18 12:15:21 +02:00
|
|
|
| grep '^[-+][^-+]'
|
|
|
|
)" || true
|
|
|
|
if [ -n "$differences" ]; then
|
|
|
|
echo
|
|
|
|
echo "Changes after running \`make oldconfig':"
|
|
|
|
echo "$differences"
|
|
|
|
echo
|
|
|
|
if echo "$differences" | grep -q '^+' ; then
|
|
|
|
exit 1
|
|
|
|
fi
|
|
|
|
fi
|