[toplevel] do not change directories to run the toplevel

Summary:
Changing directories can be surprising, don't do it as it doesn't seem to be
needed anymore. This avoids having to awkwardly pass the results dir to the
toplevel when it's in the current directory for example.

Reviewed By: mbouaziz

Differential Revision: D9215885

fbshipit-source-id: a8fd314b5
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent 9ea6d4723f
commit a566424853

@ -17,9 +17,7 @@ INCLUDE_FLAGS=$(find "$BUILD_DIR" -type d -name '*.objs' -exec printf -- '-I {}\
# file. In interactive mode $SCRIPT_DIR isn't needed # file. In interactive mode $SCRIPT_DIR isn't needed
set -x set -x
# infertop expects to be run from where dune is located "$SCRIPT_DIR"/../infer/bin/infertop.bc \
cd "$SCRIPT_DIR"/../infer
./bin/infertop.bc \
-init "$SCRIPT_DIR"/toplevel_init \ -init "$SCRIPT_DIR"/toplevel_init \
$INCLUDE_FLAGS \ $INCLUDE_FLAGS \
-I "$SCRIPT_DIR" \ -I "$SCRIPT_DIR" \

Loading…
Cancel
Save