On Monday, January 5, 2015 1:52:45 PM UTC-8, Volker Braun wrote:
>
> IMHO the only satisfactory solution to the original problem is rewriting
> it as a Python argeparse script...
>
That's what this line leads to. Really,
if [ "${1:0:11}" = "--notebook=" ] || [ "${1:0:10}" = "-notebook=" ] || [
"${1:0:3}" = "-n=" ]; then
should work just as well as the wildcard version.
--
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 [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sage-devel.
For more options, visit https://groups.google.com/d/optout.
