Apply 1 suggestion(s) to 1 file(s)

Co-authored-by: Michele Alberti <michele.alberti@cea.fr>

update_headers.sh

@@ -5,7 +5,7 @@ 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'
+  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