Add support for reading input files from the command line.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
aa49eb4b0f
commit
5d609928af
1 changed files with 13 additions and 2 deletions
|
@ -1,10 +1,21 @@
|
|||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include "version.h"
|
||||
#include "parser.h"
|
||||
using namespace lean;
|
||||
|
||||
int main() {
|
||||
int main(int argc, char ** argv) {
|
||||
std::cout << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n";
|
||||
frontend f;
|
||||
if (argc == 1) {
|
||||
return parse_commands(f, std::cin) ? 0 : 1;
|
||||
} else {
|
||||
bool ok = true;
|
||||
for (int i = 1; i < argc; i++) {
|
||||
std::ifstream in(argv[i]);
|
||||
if (!parse_commands(f, in))
|
||||
ok = false;
|
||||
}
|
||||
return ok ? 0 : 1;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue