Skip to content

Conversation

@Seasawher
Copy link
Member

Summary

  • adjust custom index.hbs for mdBook 0.4.41's async sidebar
  • add Lean playground button and restore scroll position after load
  • rely on toc.js to populate sidebar and keep scroll state
  • manually rebind sidebar fold toggles after toc.js runs so chapters expand when clicked
  • expand the active chapter on load so navigating to a page reveals its children

Testing

  • mdbook build (fails: Chapter file not found, ./README.md)
  • lake run build (fails: external command 'git' exited with code 128)
  • lake exe cache get (fails: external command 'git' exited with code 128)

https://chatgpt.com/codex/tasks/task_e_689391f06dfc832cb99905759739a1c1

@Seasawher
Copy link
Member Author

Seasawher commented Aug 6, 2025

テスト項目

  • 目次をクリックしたときの挙動が正常
  • mdbook admonish がきちんと動いている
  • 二種類のRun on lean 4 playground ボタンが動作している
  • ページ内目次が正常に動作している
  • ランダムページが正常に動作している
  • 日本語検索が正常に動作する

@Seasawher Seasawher merged commit dd768ae into main Aug 6, 2025
4 checks passed
@Seasawher Seasawher deleted the 5vux13-codex/fix-layout-issues-after-mdbook-update branch August 6, 2025 23:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants