remove now useless deprecate_file script

Villetaneuse · Nov 28, 2023 · 8f20298 · 8f20298
1 parent b06166b
commit 8f20298
Showing 1 changed file with 0 additions and 39 deletions.
diff --git a/dev/tools/deprecate_file.sh b/dev/tools/deprecate_file.sh