summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2022-01-19 19:27:00 +0000
committerDavid Allsopp <david.allsopp@metastack.com>2022-06-13 11:31:50 +0100
commit6242783cba6c129e6e886247b91b063873c6225b (patch)
treefa24cda021597a46cda35358973859a6d1921802 /tools
parent9ef03735ac472ea70bbc0c0bd1db784ef6201ba6 (diff)
downloadocaml-6242783cba6c129e6e886247b91b063873c6225b.tar.gz
Handle .refptr. symbols in check-symbol-names
Diffstat (limited to 'tools')
-rwxr-xr-xtools/check-symbol-names2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/check-symbol-names b/tools/check-symbol-names
index a8afe539d5..2cddc53d72 100755
--- a/tools/check-symbol-names
+++ b/tools/check-symbol-names
@@ -20,7 +20,7 @@ set -o pipefail
nm -A -P "$@" | LC_ALL=C awk '
# ignore caml_foo, camlFoo_bar, _caml_foo, _camlFoo_bar
-$2 ~ /^(_?caml[_A-Z])/ { next }
+$2 ~ /^(\.refptr\.)?(_?caml[_A-Z])/ { next }
# ignore local and undefined symbols
$3 ~ /^[a-zU]$/ { next }
# ignore "main", which should be externally linked