2010/1/11 John Cremona <john.crem...@gmail.com>: > Googling found me this: > http://www.phwinfo.com/forum/comp-unix-shell/392108-strip-path-get-filename.html > which appears to be a response to one Dave Kirby. > > basename does the trick, doesn't it? > > John
No, basename is not what is wanted. The 'basename' of /usr/local/bin/make would be 'make'. We need to preseve the path if someone uses one, but ignore the options. In the above case, /usr/bin/make might well be executed, when the user specified /usr/local/bin/make Dave
-- To post to this group, send an email to sage-devel@googlegroups.com To unsubscribe from this group, send an email to sage-devel+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/sage-devel URL: http://www.sagemath.org
