On Wed, May 29, 2019 at 10:16 AM Dima Pasechnik <dimp...@gmail.com> wrote: > > dash is a bit of a problem. I am not sure whether currently it is > possible to build Sage with sh==dash
hmm, scratch this. it works at least on Debian stable. > Perhaps modifying pynormaliz to actually use bash for building might > solve this. > > On Wed, May 29, 2019 at 9:15 AM Sébastien Labbé <sla...@gmail.com> wrote: > > > > > > > > On Wednesday, May 29, 2019 at 8:53:37 AM UTC+2, Samuel Lelievre wrote: > >> > >> Tue 2019-05-28 23:09:33 UTC+2, Sébastien Labbé: > >>> > >>> > >>> On Tuesday, May 28, 2019 at 1:40:45 PM UTC+2, Michael Orlitzky wrote: > >>>> > >>>> > >>>> First, can you find out where /bin/sh actually points? > >>> > >>> > >>> Sorry, I do not know how to answer this question. What command should I > >>> type? > >> > >> > >> ls -halF /bin/sh > > > > > > Here is what I get: > > > > $ ls -halF /bin/sh > > lrwxrwxrwx 1 root root 4 févr. 17 2016 /bin/sh -> dash* > > > > > > > > -- > > 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 post to this group, send email to sage-devel@googlegroups.com. > > Visit this group at https://groups.google.com/group/sage-devel. > > To view this discussion on the web visit > > https://groups.google.com/d/msgid/sage-devel/9838331c-8b7d-476a-9656-891b525b16df%40googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. -- 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 post to this group, send email to sage-devel@googlegroups.com. Visit this group at https://groups.google.com/group/sage-devel. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/CAAWYfq0oR1zAO%3DP%2BzQBdKy6UacUbbqqRrrnrobyEj_dhQ8chig%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
