test branch

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

diff --git a/helm/matita/scripts/shell_time2cents.php b/helm/matita/scripts/shell_time2cents.php
new file mode 100755 (executable)
index 0000000..4914fc2
--- /dev/null
+++ b/helm/matita/scripts/shell_time2cents.php
@@ -0,0 +1,4 @@
+<?php
+ require($argv[1]);
+ print(time_2_cents($argv[2]));
+?>