proper NULL termination;
native executable even for Linux, to avoid surprises with file managers opening executable script as text file; --HG-- rename : Admin/Linux/Isabelle => Admin/Linux/Isabelle.run