#! /bin/bash

# lines 4 contains a timestamp...
differences="$(
    diff -bU0 <(sed -e '/CONFIG_GCC_VERSION/ d' -e '/CONFIG_LD_VERSION/ d' -e '/CONFIG_CC_VERSION_TEXT/ d' -e '/^# .* is not set$/p' -e '/^$\|^#/d' "$1" | sort) \
	      <(sed -e '/CONFIG_GCC_VERSION/ d' -e '/CONFIG_LD_VERSION/ d' -e '/CONFIG_CC_VERSION_TEXT/ d' -e '/^# .* is not set$/p' -e '/^$\|^#/d' "$2" | sort) \
    | 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