From 130eac1b776248685af0590dcd6792f2d463ba67 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Sep 2021 11:31:41 +0200 Subject: [PATCH] chore: reintroduce lean.cpp in separate commit so Git doesn't freak out --- src/shell/lean.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 src/shell/lean.cpp diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp new file mode 100644 index 0000000000..c2f9a09967 --- /dev/null +++ b/src/shell/lean.cpp @@ -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); +}