Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix(shell): add missing include (#813)
This header inclusion was missing, resulting in build errors with recent versions of GCC: ``` In file included from /home/jonathan/Code/lean3/src/shell/lean_js_main.cpp:9: /home/jonathan/Code/lean3/src/shell/lean_js.h:11:32: error: ‘uintptr_t’ was not declared in this scope 11 | int emscripten_process_request(uintptr_t msg); ```
- Loading branch information