On Tue, Jan 1, 2019 at 8:25 PM Simon King <simon.k...@uni-jena.de> wrote: > > On 2019-01-01, Volker Braun <vbraun.n...@gmail.com> wrote: > > gap is standard, gap_packages is optional > > > > $ cat build/pkgs/gap/type > > standard > > $ cat build/pkgs/gap_packages/type > > optional > > I had a look at #22626, where some comments indicate that database_gap > is becoming fully *standard*. On the other hand, comments in #26856 > indicate that database_gap is merged into gap_packages,
no. database_gap is merged in gap. > thus *not* > standard. On yet another hand, #26856 removes database_gap from the > dependencies list of p_group_cohomology and also edits SPKG.txt in a > way that indicates that at least SmallGroups *is* standard. > > So, the pieces of information I got form the following picture: > "database_gap was fully merged into *two* other packages. Rumour has it > that SmallGroups is now in gap, perhaps some other parts as well (but > that's a secret), and a non-empty subset of database_gap now is in > gap_packages." That's not nice. > > If it is really the case that database_gap was split, some parts merged > into a standard package, other parts merged into an optional package, > then it would be good to have a list somewhere. > > Regards, > Simon > > -- > 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. > 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. For more options, visit https://groups.google.com/d/optout.
