#! /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

​