max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: Emscripten realpath

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-06-02 23:58:45 -04:00 • committed by Sebastian Ullrich
parent b7cd68a91e
commit 91d4011aa8
1 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/runtime/io.cpp
View file

@ -449,9 +449,7 @@ extern "C" obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) {
}
extern "C" obj_res lean_io_realpath(obj_arg fname, obj_arg) {
#if defined(LEAN_EMSCRIPTEN)
return io_result_mk_ok(fname);
#elif defined(LEAN_WINDOWS)
#if defined(LEAN_WINDOWS)
constexpr unsigned BufferSize = 8192;
char buffer[BufferSize];
DWORD retval = GetFullPathName(string_cstr(fname), BufferSize, buffer, nullptr);
@ -467,8 +465,7 @@ extern "C" obj_res lean_io_realpath(obj_arg fname, obj_arg) {
return io_result_mk_ok(mk_string(buffer));
}
#else
constexpr unsigned BufferSize = 8192;
char buffer[BufferSize];
char buffer[PATH_MAX];
char * tmp = realpath(string_cstr(fname), buffer);
if (tmp) {
obj_res s = mk_string(tmp);