Skip to content
Snippets Groups Projects

Move "classic" Prosa to rt.classic namespace and update documentation

Merged Move "classic" Prosa to rt.classic namespace and update documentation
move-to-classic into master
Merged Björn Brandenburg requested to merge move-to-classic into master
Viewing commit 8037703d
Prev Next
Show latest version
2 files
+ 11
− 12
Compare changes
  • Side-by-side
  • Inline
Files
2
  • 8037703d
    Björn Brandenburg
    cleanup create_makefile.sh · 8037703d
    Björn Brandenburg authored 
    1) rely on patch to actually patch the Makefile
2) move ineffective 'sed' hackery related to 'make validate'

Re 2), the sed script didn't actually modify the Makefile anyway
(unlear how long it has been ineffective), so let's just remove it.
scripts/Makefile.patch
+ 10
− 0
@@ -19,3 +19,13 @@
mlihtml: $(MLIFILES:.mli=.cmi)
$(SHOW)'CAMLDOC -d $@'
@@ -446,6 +449,9 @@
-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+# Prosa: include pretty documentation targets
+include scripts/coqdocjs/Makefile.coqdocjs
+
# FIXME: not quite right, since the output name is different
gallinahtml: GAL=-g
gallinahtml: html