build-dune.sh -> setup.sh

parent 0cf8461e
......@@ -12,5 +12,5 @@ echo "${DIR}/venv/dune/bin/activate"
if [ -e "${DIR}/venv/dune/bin/activate" ]; then
source "${DIR}/venv/dune/bin/activate"
else
echo "WARNING: missing virtualenv, did you call build-dune.sh?"
echo "WARNING: missing virtualenv, did you call setup.sh?"
fi
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment