From e7f4d2bed7b812a69e15896183c6801440b3dd29 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 28 Oct 2005 16:36:56 +0000
Subject: [PATCH] fix

---
 helm/matita/scripts/shell_adder.php | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100755 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
index 000000000..e0ddda95e
--- /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])); 
+?>
-- 
2.39.2