On Thu, Nov 21, 2024 at 07:39:33AM CET, Bitfox <hi@bitfox.ddns.net> said: > > BTW, what’s the difference between [[ ]] and [ ] here? I know only the > latter. IIRC, [[ ]] is a bash/zsh builtin, [ ] is /bin/[ other name of /bin/test -- Erwan David