TauTastic

Update github.ts

2

## ☕️ Reasoning This PR addresses an inconsistency in the GitHub provider within NextAuth.js. Currently, the GitHub provider fails to expose the email_verified status provided by GitHub, even though this...

### Provider type GitHub ### Environment System: OS: macOS 14.3.1 CPU: (14) arm64 Apple M3 Max Memory: 75.42 GB / 96.00 GB Shell: 5.9 - /bin/zsh Binaries: Node: 20.11.0 -...

Stop trimming '!' and '?' from tactic name. Fixes #299

5

Stop trimming '!' and '?' from tactic name. Fixes #299. I have used `main` as the base branch since I don't know how to test on `dev` since the editor...

Increase severity of `uses 'sorry'`. Fixes #276. The goal will no longer be considered completed but the actual syntax error is not displayed anywhere.

Disallowed tactics still send info messages to the client

1

I have fixed #299 so that my local build now correctly distinguishes between `apply` and `apply?` as two separate tactics. However, during testing, I noticed that disallowed tactics still send...

Potential Bug: Unintended File Access via `/api` Endpoints

1

Using any of the `/api` endpoints of the Express server, it is possible to access nearly all files within the project's directory. Below are some examples: - https://live.lean-lang.org/api/examples/mathlib-demo/build.sh - https://live.lean-lang.org/api/examples/mathlib-demo/.lake/packages/mathlib/README.md...