From 218bcaf207fbcc812f763d5a5339b281cc968afd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 23 Oct 2020 10:23:42 +0200
Subject: [PATCH] Makes update_api_doc case insensitive
---
bin/update_api_doc.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/bin/update_api_doc.sh b/bin/update_api_doc.sh
index 164a4d95714..80313ff753f 100755
--- 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
--
GitLab