Skip to content
Snippets Groups Projects
update_headers.sh 492 B
Newer Older
#!/usr/bin/env bash
NEW_DATE=$(date "+%Y")
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 -prune \) \( -type d -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