Skip to content
Snippets Groups Projects
update_headers.sh 477 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 -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