#!/bin/sh # For the MPFR team. Run this script to get a diff between the MPFR website # (mounted) and the pages in this working tree. if [ $# -ne 1 ]; then echo "Usage: $0 <website_directory>" >&2 exit 1 fi diff -x .git -x .htupdate -x lost+found -aurd "$1" "`dirname "$0"`/www"