05/11/2021 22:10, Thomas Monjalon: > The script devtools/check-dup-words.sh can detect some words > which are duplicated. After double check, it seems this script is not in the repository, probably because of the false positives. I will change this sentence in the v2.