Rename this repo to a bad pun

Changes

2 changed files (+4/-4)

• lake-manifest.json
  • @@ -91,5 +91,5 @@
    "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}], - "name": "leantest", + "name": "miscelleaneous", "lakeDir": ".lake"}
• lakefile.toml
  • @@ -1,6 +1,6 @@
    - name = "leantest" + name = "miscelleaneous" version = "0.1.0" - defaultTargets = ["leantest"] + defaultTargets = ["miscelleaneous"] [leanOptions.weak.linter] mathlibStandardSet = true
  • @@ -8,7 +8,7 @@ flexible = true
    style.longLine = false [[lean_exe]] - name = "leantest" + name = "miscelleaneous" root = "Main" [[lean_exe]]