Oh! Thanks!

Perhaps DrRacket's button should include the +m flag.

Robby


On Mon, May 3, 2021 at 10:37 AM Sam Caldwell <[email protected]> wrote:

> Ah, I meant what happens when I open up my scribble file in DrRacket and
> press the "Scribble HTML" button. Maybe it would be more accurate to
> describe that as a plugin than DrRacket itself?
>
> -Sam Caldwell
>
> On Mon, May 3, 2021 at 11:24 AM Robby Findler <[email protected]>
> wrote:
>
>> On Mon, May 3, 2021 at 10:19 AM Sam Caldwell <[email protected]> wrote:
>>
>>> When I first ran Ryan's example, the reference to `racket:let` did not
>>> resolve to the proper link. After further investigating, this appears to be
>>> due to scribble's default behavior of not loading extra cross-referencing
>>> information [1]. If instead of `raco scribble`, I run `raco scribble +m`
>>> the link does resolve to the proper location. It also appears that DrRacket
>>> uses the +m option by default.
>>>
>>>
>> Just a minor point of clarification: DrRacket uses the documentation
>> built by `raco setup`; it doesn't build the docs itself. This is the same
>> build of the docs you see with `raco docs`.
>>
>> Robby
>>
>> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/CALuKBHvJFmaJB9nf9%2BSDRAR6HUNa2pXeC0eaRfJ7VQ1quiC4_w%40mail.gmail.com
> <https://groups.google.com/d/msgid/racket-users/CALuKBHvJFmaJB9nf9%2BSDRAR6HUNa2pXeC0eaRfJ7VQ1quiC4_w%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to [email protected].
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAL3TdONURvPexFUbFeRPeNap8Y%2B4cRjRS-XBMWPK-hOPQFqVGQ%40mail.gmail.com.

Reply via email to