Closed andrealinux1 closed 2 years ago
When invoking orc shell, under the hood this command to retrieve the shell used: https://github.com/revng/revng-orchestra/blob/fbcef955f6e5346c010c1c6b421f8f1759ec15d0/orchestra/cmds/shell.py#L63
orc shell
If, by accident and misconfiguration, no shell is defined for the user, the command simply returns with no significant debug message. We could improve this behavior by showing a warning when there is no shell for the current session.
Solved by #44
fcremo
commented
2 years ago
When invoking
orc shell, under the hood this command to retrieve the shell used: https://github.com/revng/revng-orchestra/blob/fbcef955f6e5346c010c1c6b421f8f1759ec15d0/orchestra/cmds/shell.py#L63If, by accident and misconfiguration, no shell is defined for the user, the command simply returns with no significant debug message. We could improve this behavior by showing a warning when there is no shell for the current session.