Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Sophie Quinton
rt-proofs
Commits
170ca73b
Commit
170ca73b
authored
Jul 13, 2016
by
Björn Brandenburg
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix Makefile on OS X
The BSD version of `find` needs to be given '.' as the search path.
parent
52dc407a
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
2 additions
and
2 deletions
+2
-2
Makefile
Makefile
+1
-1
create_makefile.sh
create_makefile.sh
+1
-1
No files found.
Makefile
View file @
170ca73b
...
...
@@ -341,7 +341,7 @@ uninstall: uninstall_me.sh
clean
::
rm
-f
$(OBJFILES)
$(OBJFILES:.o=.native)
$(NATIVEFILES)
find
.
-name
.coq-native
-type
d
-empty
-delete
find
-name
"*.vo"
-delete
-o
-name
"*.glob"
-delete
-o
-name
"*.v.d"
-delete
-o
-name
"*.vio"
-delete
-o
-name
"*.old"
-delete
-o
-name
"*.beautified"
-delete
find
.
-name
"*.vo"
-delete
-o
-name
"*.glob"
-delete
-o
-name
"*.v.d"
-delete
-o
-name
"*.vio"
-delete
-o
-name
"*.old"
-delete
-o
-name
"*.beautified"
-delete
rm
-f
all.ps all-gal.ps all.pdf all-gal.pdf all.glob
$(VFILES:.v=.glob)
$(VFILES:.v=.tex)
$(VFILES:.v=.g.tex)
all-mli.tex
-
rm
-rf
html mlihtml uninstall_me.sh
...
...
create_makefile.sh
View file @
170ca73b
...
...
@@ -11,4 +11,4 @@ sed -i 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makef
sed
-i
's|-interpolate -utf8|-interpolate -utf8 --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g'
Makefile
# Fix 'make clean' to remove all binary files, regardless of name
sed
-i
's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g'
Makefile
sed
-i
's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find
.
-name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g'
Makefile
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment