diff --git a/dev.xml b/dev.xml index b7165721ead743637be4340c0f0c08089e18dcdb..16f7dbeda096d6fb48dec791ff1aaf04379f17bd 100644 --- a/dev.xml +++ b/dev.xml @@ -54,7 +54,7 @@ <project path="hedge" name="inducer/hedge.git" /> <!-- time integration --> - <project path="hedge" remote="gitlab" name="inducer/leap.git" /> + <project path="leap" remote="gitlab" name="inducer/leap.git" /> <!-- random stuff --> <project path="experiments" remote="gitlab" name="inducer/experiments.git" />