diff BUGS @ 737:8a8873e7a552

Make shell command and its option rc file options instead of hardcoded strings. This allows users to modify the shell command that execute "editors". Two new options appear in rc file: - shell.path (default to "/bin/sh") - shell.options (default to "-c") These options can only be changed from the rc file, not at runtime. Tests are made to check that shell.path is not empty and lead to an executable file.
author zas_
date Thu, 22 May 2008 20:22:13 +0000
parents 9e54275835fb
children
line wrap: on
line diff