> pushd works in my system (Ubuntu) if I use it directly, but if I use it
> as "sudo pushd" it doesn't work. In Ubuntu one never logs in as
> superuser, so what I have to do is "sudo make install".
Is it really necessary on Ubuntu to run make install with root
privileges? On Debian I added my (otherwise unprivileged) user to
group staff. This is enough to install maxima to /usr/local/*
and has the advantage that a broken install script can't harm the
rest of my system.
Of course fixing make install to be sudo friendly is useful too.
Harald