Ditto : +1 for optional Le mercredi 19 juin 2019 09:44:33 UTC+2, vdelecroix a écrit : > > +1 for optional > > Le 19/06/2019 à 09:15, Dima Pasechnik a écrit : > > Sure, let us make it optional. > > > > On Wed, 19 Jun 2019 at 00:15, Isuru Fernando <isu...@gmail.com > <javascript:>> wrote: > > > >> Hi, > >> > >> Rubiks package is a combination of 3 packages with lots of patches to > the > >> build system > >> > >> Keeping it standard requires package managers to package this strange > >> package of 3 packages and wastes time if nobody is using it. > >> > >> Users can use gap to solve the rubik's cube or install the rubiks spkg > if > >> sage was built using source. > >> > >> > >> Isuru > >> > >> -- > >> 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-...@googlegroups.com <javascript:>. > >> To post to this group, send email to sage-...@googlegroups.com > <javascript:>. > >> 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/CA%2B01voNoM3twbkxpJp6JnJbwsHh5FDRumjCSrVAy_kB1yP5m-g%40mail.gmail.com > > >> < > https://groups.google.com/d/msgid/sage-devel/CA%2B01voNoM3twbkxpJp6JnJbwsHh5FDRumjCSrVAy_kB1yP5m-g%40mail.gmail.com?utm_medium=email&utm_source=footer> > > > >> . > >> 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/932aa80a-e88e-45f8-b319-6301a4a47813%40googlegroups.com. For more options, visit https://groups.google.com/d/optout.
