diff --git a/Maintenance/infrastructure/cgal.geometryfactory.com/bin/dump_crontab b/Maintenance/infrastructure/cgal.geometryfactory.com/bin/dump_crontab index 4e682ab1451..c383fc404b4 100755 --- a/Maintenance/infrastructure/cgal.geometryfactory.com/bin/dump_crontab +++ b/Maintenance/infrastructure/cgal.geometryfactory.com/bin/dump_crontab @@ -1,6 +1,6 @@ #!/bin/zsh -cd $HOME/CGAL/next/Maintenance/infrastructure/cgal.geometryfactory.com/ +cd $HOME/infrastructure crontab -l >| crontab if [ -d ../../../.git ]; then git pull --quiet