You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I am trying to make my project website (eg https://teorth.github.io/pfr) generate a dependency graph of all files within my project (eg PFR) for the purpose of knowing which files to prioritise the upstreaming of. Typically, some files still contain sorry and are not ready to be upstreamed yet.
My current setup is to run lake exe graph foo.pdf and make foo.pdf available on the website. If there was a --sorry flag or something like that, I could put the resulting PDF on my website without any further postprocessing.
The text was updated successfully, but these errors were encountered:
I am trying to make my project website (eg https://teorth.github.io/pfr) generate a dependency graph of all files within my project (eg PFR) for the purpose of knowing which files to prioritise the upstreaming of. Typically, some files still contain
sorryand are not ready to be upstreamed yet.My current setup is to run
lake exe graph foo.pdfand makefoo.pdfavailable on the website. If there was a--sorryflag or something like that, I could put the resulting PDF on my website without any further postprocessing.The text was updated successfully, but these errors were encountered: