remove filePlay functionality

lean-ja · Mar 17, 2024 · de9c9af · de9c9af
1 parent 04b55fd
commit de9c9af
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 35 deletions.
diff --git a/assets/filePlay.js b/assets/filePlay.js
diff --git a/book.toml b/book.toml
@@ -12,14 +12,10 @@ build-dir = "book"
 
 [output.html]
 git-repository-url = "https://github.com/Seasawher/lean99"
-edit-url-template = "https://raw.githubusercontent.com/Seasawher/lean-book/main/{path}"
 additional-js = [
   # Add "Run on Lean4 Playground" button to each code block
   "assets/blockPlay.js",
 
-  # Add "Run on Lean4 Playground" button to each page
-  "assets/filePlay.js",
-
   # Improve search functionality
   "assets/fzf.umd.js",
   "assets/elasticlunr.js"