Skip to content

Conversation

@Seasawher
Copy link
Member

Summary

  • move toc.js to head to avoid empty sidebar after mdbook 0.4.42
  • adjust comment regarding sidebar initialization

Testing

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

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

@Seasawher
Copy link
Member Author

Seasawher commented Aug 7, 2025

テスト項目

  • 目次をクリックしたときの挙動が正常
  • mdbook admonish がきちんと動いている
  • 二種類のRun on lean 4 playground ボタンが動作している
  • ページ内目次が正常に動作している
  • ランダムページが正常に動作している
  • 日本語検索が正常に動作する
  • 開発者ツールを開き、コンソールにエラーや警告が出ていないことを確認する

@Seasawher Seasawher merged commit 4b69295 into main Aug 7, 2025
4 checks passed
@Seasawher Seasawher deleted the codex/fix-sidebar-toc-display-issue branch August 7, 2025 12:58
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