diff options
| author | letouzey | 2010-03-18 19:44:14 +0000 |
|---|---|---|
| committer | letouzey | 2010-03-18 19:44:14 +0000 |
| commit | 26cb451aea4dd24f4f0fe31068af219cc30c0e07 (patch) | |
| tree | 4ae29ef24cfec933822826fbb7faa72ee6d613ac /scripts | |
| parent | 68352782e99387e7c0b0a87d764ce78b2de7890a (diff) | |
Makefile.build: (slightly) more robust sed invocation for parsing camlp4deps/use lines
The build error Y. Makarov recently reported on coq-club was caused by some
.ml4 having dos-style end-of-line in his source-tree, and hence \r appearing in
the camlp4o commandline. We now simply discard what appears after camlp4xxx "...".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12871 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions