diff --git a/lib/resource-1.0/Makefile b/lib/resource-1.0/Makefile index 33e33764b..a7e356b0a 100644 --- a/lib/resource-1.0/Makefile +++ b/lib/resource-1.0/Makefile @@ -56,5 +56,5 @@ gfdoc: mv ../prelude/*.html doc/gfdoc clean: - rm */*.gfc */*.gfr */*.gf~ + -rm */*.gfc */*.gfr */*.gf~