diff --git a/dev.xml b/dev.xml index 85c32e162b1f73fdbe81f1c0248d7cce905f1e11..b7165721ead743637be4340c0f0c08089e18dcdb 100644 --- a/dev.xml +++ b/dev.xml @@ -53,6 +53,9 @@ <!-- DG --> <project path="hedge" name="inducer/hedge.git" /> + <!-- time integration --> + <project path="hedge" remote="gitlab" name="inducer/leap.git" /> + <!-- random stuff --> <project path="experiments" remote="gitlab" name="inducer/experiments.git" /> <project path="photonics-dg" remote="gitlab" name="photonics/photonics-dg.git" />