summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2022-01-20 16:00:33 +0000
committerDavid Allsopp <david.allsopp@metastack.com>2022-06-13 11:31:50 +0100
commit43f81b84daac960a28e7e4113cf69f3f3b8d9b8a (patch)
treed4705f4e693efccdc79959083e9997b1f2666b39 /tools
parent9e1d5fc4aa081d66cac6ac70fbb01059d20157ff (diff)
downloadocaml-43f81b84daac960a28e7e4113cf69f3f3b8d9b8a.tar.gz
Allow functions in win32unix to begin with win_
Diffstat (limited to 'tools')
-rwxr-xr-xtools/check-symbol-names2
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/check-symbol-names b/tools/check-symbol-names
index 74f01f3e55..69971b291c 100755
--- a/tools/check-symbol-names
+++ b/tools/check-symbol-names
@@ -28,6 +28,8 @@ $3 ~ /^[a-zU]$/ { next }
# ignore "main", which should be externally linked
$2 ~ /^_?main$/ { next }
$2 ~ /^_?wmain$/ { next }
+# Ignore win_ in Unix library
+$1 ~ /\/unix/ && $2 ~/^_?win_/ { next }
# uerror is too widely known!
$2 ~ /^_?uerror$/ { next }
# for x86 PIC mode