Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit a583ad8f authored by POTTIER Francois's avatar POTTIER Francois

Update GNUmakefile to include .messages file in the tar archive.

parent 5f5f18e5
......@@ -99,7 +99,7 @@ package: clean
@ rm -fr $(PACKAGE)
@ mkdir -p $(PACKAGE)/src
@ cp -fr src/*.ml{,i,y,l,pack} src/Makefile src/META $(PACKAGE)/src
@ cp -fr src/*.ml{,i,y,l,pack} src/*.messages src/Makefile src/META $(PACKAGE)/src
@ grep -v my_warnings src/_tags > $(PACKAGE)/src/_tags
@ $(MAKE) -C $(PACKAGE)/demos clean
# Insert headers.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment