Newer
Older
OLD_DATE=$(sed "5q;d" src/main.ml | awk '{print $4}')
if [ "$OLD_DATE" != "$NEW_DATE" ]; then
echo "Replacing $OLD_DATE by $NEW_DATE in headers."
find . -type d \( -name .git -o -name _build \) -prune -o -type f -print0 | xargs -0 sed -i 's/(C) '"${OLD_DATE}"'/(C) '"${NEW_DATE}"'/g'
echo "Done."
exit 0
else
echo "Year $OLD_DATE in header src/main.ml is current date, no need to update the headers."
exit 0
fi