diff --git a/tlatools/test/tla2sany/drivers/Github429Test.java b/tlatools/test/tla2sany/drivers/Github429Test.java index f0508ac553f59356554a42341e95907faa92c127..11d70a05f04fa397c890d70709fb7ee827080aaf 100644 --- a/tlatools/test/tla2sany/drivers/Github429Test.java +++ b/tlatools/test/tla2sany/drivers/Github429Test.java @@ -5,6 +5,7 @@ import org.junit.Before; import org.junit.Test; import tla2sany.modanalyzer.SpecObj; +import tlc2.tool.CommonTestCase; import util.SimpleFilenameToStream; import util.ToolIO; @@ -15,7 +16,7 @@ public class Github429Test { @Before public void setUp() throws Exception { // create a model and initialize - moduleSpec = new SpecObj("test-model/Github429.tla", new SimpleFilenameToStream()); + moduleSpec = new SpecObj(CommonTestCase.BASE_PATH + "Github429.tla", new SimpleFilenameToStream()); SANY.frontEndInitialize(moduleSpec, ToolIO.out); }