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

chore(tests/lean/parser1): restore #exit...

Browse source
This commit is contained in:
Sebastian Ullrich 2018-12-12 11:06:52 +01:00
parent ad11a8807f
commit 1d524476b7
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/parser1.lean
View file

@ -137,6 +137,7 @@ def run_frontend (input : string) : except_t string io unit := do
let stx := stx.update_leading input,
io.println "result:",
io.println (to_string stx)-/
#exit
-- slowly progressing...
set_option profiler true