summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2022-05-25 11:45:28 +0100
committerDavid Allsopp <david.allsopp@metastack.com>2022-06-13 11:31:50 +0100
commit5a701f2151737a2869544726cf450ef661913627 (patch)
tree137196d81117057ad52317834b8f7da6316ab219 /tools
parent88d311eba0f8d54f3ab055e908ae34b029d91f89 (diff)
downloadocaml-5a701f2151737a2869544726cf450ef661913627.tar.gz
Rename renaming win_ primitives to unix_
Diffstat (limited to 'tools')
-rwxr-xr-xtools/check-symbol-names2
1 files changed, 0 insertions, 2 deletions
diff --git a/tools/check-symbol-names b/tools/check-symbol-names
index 91f321f453..3ad64216ca 100755
--- a/tools/check-symbol-names
+++ b/tools/check-symbol-names
@@ -28,8 +28,6 @@ $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