Issues in docs on iphone

Stream: general

[Jason Rute]

The markdown in https://leanprover-community.github.io/lean4-metaprogramming-book/ shows up strange on my iPhone (both safari and Firefox apps). 34580014-BF8E-4AFA-A88A-05EA4BF9A744.png

[Jason Rute]

I’ve seen this before in some of the other docs like the Lean manual, but it seems fixed now in the Lean manual.

[Adam Topaz]

It looks fine on my iPhone (on Firefox, dark mode obviously)
890774A0-F14C-47D4-A523-9073F31D725D.png

[Jason Rute]

Also the hamburger menu doesn’t work for me on that page.

[Adam Topaz]

Hamburger works fine for me

[Jason Rute]

Nor on https://lean-lang.org/lean4/doc/whatIsLean.html

[Jason Rute]

Wow. I guess it’s just my phone.

[Adam Topaz]

The fact that both safari and Firefox fail in similar ways is suspicious

[Mario Carneiro]

on iphone, all browsers are safari

[Mario Carneiro]

firefox on iOS is just a safari skin

[Mario Carneiro]

(this is part of the iPhone store terms of service)

[Adam Topaz]

I had no idea!

[Julian Berman]

Jason if you visit some other random mdbook thing I assume you get the same problem? (It'd seem likely if both projects are broken, just asking anyhow)

[Julian Berman]

E.g. the rust docs or something, sec, a link is...

[Julian Berman]

Well or mdbook's docs itself -- https://rust-lang.github.io/mdBook/

[Jason Rute]

Most of the other Lean documentation. Like TPIL and FPIL and the Lean Manual look fine. Although I did in the past have some problems with at least some of them so maybe it is a caching thing. The hamburger menu also works fine on many other Lean md pages.