Re: [sage-devel] Make JupyterLab a standard package
On Tuesday, March 6, 2018 at 4:58:53 AM UTC-5, Jeroen Demeyer wrote: > > On 2018-03-06 00:29, Samuel Lelièvre wrote: > > I opened a ticket to make JupyterLab a standard package: > > > > https://trac.sagemath.org/ticket/24904 > > > > Any opinions? > > Shouldn't it be an optional package first? > > Ordinarily, yes. -- 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.
[sage-devel] Somebody relying on make micro_release?
Hi, in #24655 I am working on docker images of Sage. One thing I am trying to achieve is to make the images smaller than they currently are. (I am now at 577MB with all doctests passing.) I assume that the `micro_release` target of our Makefile is meant for that purpose: drop everything that is not essential to running Sage. But I am not sure, maybe somebody is using this in their workflow for some other purposes and if I change that target their workflow might break now? If you are currently relying on `micro_release`, please have a look at the proposed changed at https://gitlab.com/saraedum/sage/blob/ci/Makefile#L90 and comment on #25655. cheers, julian -- 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.
Re: [sage-devel] Re: Git push issues
On Tue, Mar 6, 2018 at 11:24 PM, Luca De Feo wrote: >> No problem. And this was a mistake *I* made. This is a side-effect I >> did not consider and might want to think more about how to prevent... > > GitHub forbids using an ssh key twice. It seems the only reasonable thing to > do. Yes, I'm adding that restriction to the SSH keys plugin for the next updated. -- 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.