Make shell command and its option rc file options instead of hardcoded strings.

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.