Re: [sage-devel] Make JupyterLab a standard package

[kcrisman]

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?

[Julian Rüth]

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

[Erik Bray]

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.