On Thu, May 19, 2016 at 10:16:36PM -0400, Hendrik Boom wrote:
> On Fri, Apr 22, 2016 at 08:40:04PM -0400, Matthias Felleisen wrote:
> >
> > > On Apr 22, 2016, at 8:36 PM, Hendrik Boom wrote:
> > >
> > > It seems scribble likes to put its output where the document source is,
> > > with a differe
On Fri, Apr 22, 2016 at 08:40:04PM -0400, Matthias Felleisen wrote:
>
> > On Apr 22, 2016, at 8:36 PM, Hendrik Boom wrote:
> >
> > It seems scribble likes to put its output where the document source is,
> > with a different file extension.
> >
> > I like to separate my source code from generat
> On Apr 22, 2016, at 5:36 PM, Hendrik Boom wrote:
>
> It seems scribble likes to put its output where the document source is,
> with a different file extension.
>
> I like to separate my source code from generated files.
>
> (1) How can I tell scribble to place the generated html into a
> dif
> On Apr 22, 2016, at 8:36 PM, Hendrik Boom wrote:
>
> It seems scribble likes to put its output where the document source is,
> with a different file extension.
>
> I like to separate my source code from generated files.
>
> (1) How can I tell scribble to place the generated html into a
> d
It seems scribble likes to put its output where the document source is,
with a different file extension.
I like to separate my source code from generated files.
(1) How can I tell scribble to place the generated html into a
different directory? Is there a command line option for this?
(2) Ar
5 matches
Mail list logo