summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--stdlib/.cvsignore1
-rw-r--r--stdlib/Makefile2
2 files changed, 1 insertions, 2 deletions
diff --git a/stdlib/.cvsignore b/stdlib/.cvsignore
index 1f035fa00..343f6abd6 100644
--- a/stdlib/.cvsignore
+++ b/stdlib/.cvsignore
@@ -3,3 +3,4 @@ camlheader_ur
labelled-*
caml
*.annot
+sys.ml
diff --git a/stdlib/Makefile b/stdlib/Makefile
index ec938f701..70fc05a01 100644
--- a/stdlib/Makefile
+++ b/stdlib/Makefile
@@ -91,9 +91,7 @@ camlheader camlheader_ur: header.c ../config/Makefile
fi
sys.ml: sys.mlp ../VERSION
- @rm -f sys.ml
sed -e "s|%%VERSION%%|`head -1 ../VERSION`|" sys.mlp >sys.ml
- @chmod -w sys.ml
clean::
rm -f sys.ml