Fix public mirror

It seems that git grep is limited to 140 characters. One of the recent MRs had a line in its commit message which surpassed this limit. Since then the public mirror doesn't seem to have been running. This MR truncates the line passed to grep to 140 characters and fixes the blockage.

See merge request gysela-developpers/gyselalibxx!769

--------------------------------------------

bin/public_mirror

@@ -37,11 +37,13 @@ last_message_public=$(git log -1 --pretty=%s%n%n%b)
 git_log_options="git log --all-match -F --pretty=%H"
 while IFS= read -r line
 do
-    if [ -n "$line" ]
-    then
-      line=${line//"'"/"'\"'\"'"}
-      git_log_options="${git_log_options} --grep='$line'"
-    fi
+    while [ -n "$line" ]
+    do
+      truncated_line=${line:0:140}
+      quoted_line=${truncated_line//"'"/"'\"'\"'"}
+      git_log_options="${git_log_options} --grep='${quoted_line}'"
+      line=${line:140}
+    done
 done <<< ${last_message_public}
 git checkout ${current_SHA}