Makes update_api_doc case insensitive

17ce379f · Allan Blanchard · 2e793f8e · 17ce379f
Commit 17ce379f authored Oct 23, 2020 by Allan Blanchard
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

bin/update_api_doc.sh bin/update_api_doc.sh +1 -1

No files found.
--- a/bin/update_api_doc.sh
+++ b/bin/update_api_doc.sh
@@ -7,5 +7,5 @@ if test -z "$next"; then
  echo "\$ ./bin/update_api_doc.sh <NEXT>"
  echo "See the Release Management Documentation for an example."
 else
-  find src -name '*.ml*' -exec sed -i -e "s/Frama-C+dev/${next}/g" '{}' ';'
+  find src -name '*.ml*' -exec sed -i -e "s/Frama-C+dev/${next}/gI" '{}' ';'
 fi