mailing-list for TeXmacs Users

[Giovanni Piredda <address@hidden>]

I am using 1.99.14

I must have made a mistake in the pushing of my changes to the 
repository I forked, because git recognized the changed html file, but 
not the changed tm file. I will try again.

G.

On 09.11.20 18:06, Massimiliano Gubinelli wrote:
> Dear Giovanni,
>   for a pull request I just need the .tm since the .html will be anyway 
> generated automatically. There is no reason to add the .html in the pull 
> request. Just make a commit with your changes and additions. ANd then PR that 
> commit.
>
> Which version of TeXmacs are you using?
>
> Max
>
>
> > On 9. Nov 2020, at 16:08, Giovanni Piredda <address@hidden> wrote:
> >
> > I haven't figured out how to copy the diff from the pull request webpage 
> > (maybe I could have done that locally), so I submitted the pull request so 
> > that you can check the diff from your computer.
> >
> > By the way I have seen that only the html file is changed, not the tm, this 
> > means I have to improve how I push changes to git (but I'll figure it out on 
> > my own).
> >
> > G.
> >
> > On 09.11.20 15:21, Massimiliano Gubinelli wrote:
> > > Can you show the diff? I'm using the svn version of TeXmacs but apart from 
> > > that nothing fancy.
> > >
> > > m
> > >
> > >
> > >
> > > > On 9. Nov 2020, at 14:23, Giovanni Piredda <address@hidden> wrote:
> > > >
> > > >
> > > > On 08.11.20 16:26, Giovanni Piredda wrote:
> > > > > Hi Massimiliano,
> > > > >
> > > > > this is very nice.
> > > > >
> > > > > I think in the next few days I will try and post a small article.
> > > > Do I need a style file which is not contained in the standard TeXmacs distribution? I 
> > > > started (did not complete) a pull request now and in the changes summary I see many 
> > > > additions in the head of the html document. I wonder if it is why in my local copy 
> > > > TeXmacs is using a different style file for generating the html? (Perhaps this is what 
> > > > Joris referred to in the message on the missing "notes" style file).