fix

[helm.git] / helm / matita / scripts / shell_adder.php

diff --git a/helm/matita/scripts/shell_adder.php b/helm/matita/scripts/shell_adder.php
new file mode 100755 (executable)
index 0000000..e0ddda9
--- /dev/null
+++ b/helm/matita/scripts/shell_adder.php
@@ -0,0 +1,5 @@
+#!/usr/bin/php4
+<?php
+ require($argv[1]);
+ print(sum_time($argv[2], $argv[3])); 
+?>