diff --git a/conf/options b/conf/options new file mode 100644 index 0000000000000000000000000000000000000000..2bfe291c65e67769587065850565beee33100129 --- /dev/null +++ b/conf/options @@ -0,0 +1 @@ +outdir +b/out/