X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fpatch_deps.sh;h=dbdd27c1111489c9511ff7c18d6cf12868065579;hb=a7063fc0997a9d9eae6c329443e67ab92c4b6a0f;hp=2abbbeab10308c2f01458b8209390f5f42614691;hpb=9b8a57ace85bca07520ba9434e67051d86e492f6;p=helm.git

diff --git a/helm/ocaml/patch_deps.sh b/helm/ocaml/patch_deps.sh
index 2abbbeab1..dbdd27c11 100755
--- a/helm/ocaml/patch_deps.sh
+++ b/helm/ocaml/patch_deps.sh
@@ -1,16 +1,39 @@
 #!/bin/sh
 # script args: source_file target_file
 
-use_clusters='yes'
+use_clusters='no'
+if [ ! -z "$USE_CLUSTERS" ]; then
+  use_clusters=$USE_CLUSTERS
+fi
 
 # args: file snippet
 # file will be modified in place
 include_dot_snippet ()
 {
-  echo "Adding to $1 graphviz snipet $2 ..."
+  echo "Adding to $1 graphviz snippet $2 ..."
   sed -i "/digraph/r $2" $1
 }
 
+# args: stats file
+# file will be modified in place
+include_loc_stats ()
+{
+  echo "Adding to $1 KLOCs stats from $2 ..."
+  tmp=`mktemp tmp.stats.XXXXXX`
+  for l in `cat $2`; do
+    module=$(basename $(echo $l | cut -d : -f 1))
+    stat=$(echo $l | cut -d : -f 2)
+    if [ "$stat" = "LOC" ]; then
+      locs=$(echo $l | cut -d : -f 3)
+      klocs=$(echo "scale=1; $locs / 1000" | bc)
+      if [ "$klocs" = "0" ]; then klocs=".1"; fi
+      printf '  %s [label="%s\\n%s klocs"];\n' $module $module $klocs >> $tmp
+    fi
+  done
+  include_dot_snippet $1 $tmp
+  rm $tmp
+}
+
 # args: file patch
 apply_patch ()
 {
@@ -21,6 +44,7 @@ apply_patch ()
 }
 
 cp $1 $2
+include_loc_stats $2 .stats
 apply_patch $2 deps.patch
 include_dot_snippet $2 daemons.dot
 if [ "$use_clusters" = "yes" ]; then