Hello, FriCAS just cloned, commit (1b5c139) and installed with --prefix=/home/user/.local
Looking at the different output modes in FriCAS, I tried the showeditor option, output from ')show' in an editor. GVim: (1) -> )sh SINT Unable to open directory to be removed rmdir failed: Not a directory Unable to open directory to be removed rmdir failed: Not a directory (1) -> Directly two empty gvim (gvim is not supported, I know). With export FRICASEDITOR=emacs (1) -> )set output showedit on (1) -> )sh SINT Unable to open directory to be removed rmdir failed: Not a directory Unable to open directory to be removed rmdir failed: Not a directory (1) -> After you close the first empty emacs, it restarts one, empty also. That scared me a little bit. What is it trying to delete... Default settings: (1) -> )set output showeditor on (1) -> )sh SINT Unable to open directory to be removed rmdir failed: Not a directory Warning: environment variable FRICASEDITOR not set. Launching 'less' in an 'xterm'. Press space to continue, 'q' to quit. Warning: environment variable FRICASEDITOR not set. Launching 'less' in an 'xterm'. Press space to continue, 'q' to quit. Again, a first window, here an Xterm, with the SINT domain opened by less. After pressing 'q', like emacs, another less in an xterm is started, but here SINT is also loaded in less. - Greg BTW: do you happen to know a very simple graphical text editor, with very few libraries needed, compatible. Opening something with a 14'' laptop in an xterm becomes illisible to (too small fonts by default and not very practical). Using Windows has some goodness... I have no Linux desktop environment and I do not need one in WSL. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAHnU2dZdeEJqRJXmGRNmHfOyC2N8SA52GeKAaL3WyLBL5u9BUw%40mail.gmail.com.
