Skip to content

Commit 09f23da

Browse files
Request stage0 update from CI
1 parent 646ad3c commit 09f23da

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

stage0/src/stdlib_flags.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
#include "util/options.h"
22

3+
// Please do a stage0 update, CI
4+
35
namespace lean {
46
options get_default_options() {
57
options opts;

0 commit comments

Comments
 (0)