You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
So according to my Googling, there is no good way on Linux to determine the default terminal emulator AFAIK. (I was hoping that there would be some equivalent of xdg-open that would open the default terminal, but there is not.)
In my opinion, adding yet another terminal to the list of hard coded terminals is undesirable. However, Debian systems, including Ubuntu and elementary OS, have the "update alternatives" system which provides an alias x-terminal-emulator that points to the default terminal emulator. On elementary OS, x-terminal-emulator points to io.elementary.terminal.
Would it therefore be reasonable to add x-terminal-emulator to the list of hard-coded executables so that x-terminal-emulator is tried before others? This should help address the issue on Debian-based distros such as elementary OS.
Submitting a MiKTeX problem report
elementary OS 6.1 is a derivative of Ubuntu 20.04 LTS with a different desktop environment.
When I open the MiKTeX Console and click the terminal icon (shown in screenshot below), nothing happens.
On elementary OS, the default terminal is the executable
io.elementary.terminal
.I cannot find anywhere on the Settings pane to configure the terminal used. Is there somewhere this can be set in a configuration file?
Note that the button to launch TeXworks works as expected.
Here is the MiKTeX installation report:
miktex-report.txt
The text was updated successfully, but these errors were encountered: