Merge branch 'impr_find_unused_symbols' into 'main'

small improvement to script "find_unused_symbols.sh"

See merge request !950