In SERVER-44458 I introduced a command-line wrapper script for TLC, the TLA+ model-checker. The script is called model-check.sh. Its purpose is to make it easy for humans to run TLC with predefined model-checking parameters, and eventually to do the same in Evergreen (SERVER-45416).

For simplicity, the first version used a Linux-only method for determining the number of CPU cores. On other platforms the script would fail.

I've changed my mind, I think it would be nice to run this script on any platform.