[Pkg-ocaml-maint-commits] [SCM] frama-c packaging branch, master, updated. debian/20081201.dfsg-1-6-g8e9101e

[Mehdi Dogguy]

The following commit has been merged in the master branch:
commit 2a781c9285d2c18ce0114e020e232b0ab69b3ff7
Author: Mehdi Dogguy <dogguy at pps.jussieu.fr>
Date:   Wed Jun 3 08:19:09 2009 +0200

    Update patch to not install cmxs on non-native archs

diff --git a/debian/patches/0006-Do-not-install-non-existant-files.patch b/debian/patches/0006-Do-not-install-non-existant-files.patch
index 2b81c0f..cb4a337 100644
--- a/debian/patches/0006-Do-not-install-non-existant-files.patch
+++ b/debian/patches/0006-Do-not-install-non-existant-files.patch
@@ -3,14 +3,22 @@ Date: Tue, 12 May 2009 17:51:22 +0200
 Subject: [PATCH] Do not install non-existant files
 
 ---
- Makefile.in |    2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
+ Makefile.in |    6 +++---
+ 1 files changed, 3 insertions(+), 3 deletions(-)
 
 diff --git a/Makefile.in b/Makefile.in
-index 80a7bee..abd55a3 100644
+index 80a7bee..9e2aa76 100644
 --- a/Makefile.in
 +++ b/Makefile.in
-@@ -2043,7 +2043,7 @@ install:
+@@ -2037,13 +2037,13 @@ install:
+ 	  $(CP) -R doc/manuals $(DESTDIR)$(datadir); \
+         fi
+ 	if [ -d lib/plugins -a $(PLUGIN_DYN_EXISTS) = "yes" ]; then \
+-	  $(CP)  $(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_CMX_LIST) \
+-	         $(PLUGIN_DYN_GUI_CMO_LIST) $(PLUGIN_DYN_GUI_CMX_LIST) \
++	  $(CP)  $(wildcard $(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_CMX_LIST) \
++	         $(PLUGIN_DYN_GUI_CMO_LIST) $(PLUGIN_DYN_GUI_CMX_LIST)) \
+ 		 $(DESTDIR)$(plugindir); \
  	fi
  # 	line below does not work if INCLUDES contains twice the same directory
  #       Do not attempt to copy gui interfaces if gui is disabled

-- 
frama-c packaging