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.
