#! /bin/bash

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