P.S: Sorry, there was a typo, "$SAGE_LOCAL/sage" should read "$SAGE_LOCAL/bin/sage"
On Mon, May 16, 2022 at 4:35 AM ph h <hohoang...@gmail.com> wrote: > Dear All, > > Please find appended below a snippet from $SAGE_ROOT/sage. > > Would it be nice if "$SAGE_LOCAL/sage" could be used without assumptions > instead of "$SAGE_ROOT/local/bin/sage" with the assumption that 'SAGE_LOCAL > is the "local" subdirectory' > > BTW, should "$SAGE_LOCAL/sage" be the first choice if it is ready to run? > > Thank you for your enlightenment > > Regards, > > phiho > > <$SAGE_ROOT/sage> > # Run the actual Sage script > if [ -x "$SAGE_ROOT/src/bin/sage" ]; then > exec "$SAGE_ROOT/src/bin/sage" "$@" > elif [ -x "$SAGE_ROOT/local/bin/sage" ]; then # if in a stripped binary > # Note in this case we assume that SAGE_LOCAL is the "local" > subdirectory > exec "$SAGE_ROOT/local/bin/sage" "$@" > else > echo >&2 "$0: no Sage installation found in \$SAGE_ROOT=$SAGE_ROOT" > exit 1 > fi > </$SAGE_ROOT/sage> > > -- > You received this message because you are subscribed to the Google Groups > "sage-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sage-devel+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sage-devel/8a705a39-977c-4fcb-b1f4-5d38b490f3e1n%40googlegroups.com > <https://groups.google.com/d/msgid/sage-devel/8a705a39-977c-4fcb-b1f4-5d38b490f3e1n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/CALZQg1bkirqCC%2BLc8L8cvSJtSo_VXdhUc3anMBHt2ackW4F8JA%40mail.gmail.com.
