chore: reintroduce lean.cpp in separate commit so Git doesn't freak out
This commit is contained in:
parent
b3bb2bac97
commit
130eac1b77
1 changed files with 16 additions and 0 deletions
16
src/shell/lean.cpp
Normal file
16
src/shell/lean.cpp
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
/*
|
||||
Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Sebastian Ullrich
|
||||
*/
|
||||
|
||||
// The actual main function is in `util/shell.cpp` and compiled into `libleanshared` to avoid issues with cross-lib C++.
|
||||
// It will eventually be replaced by Lean code anyway.
|
||||
// We put `main` in this separate file included only in `lean` so linking against `libleanshared` does not accidentally use it.
|
||||
|
||||
extern "C" int lean_main(int argc, char ** argv);
|
||||
|
||||
int main(int argc, char ** argv) {
|
||||
return lean_main(argc, argv);
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue