aboutsummaryrefslogtreecommitdiff
path: root/htmldoc/buildlibgraph
diff options
context:
space:
mode:
authorEnrico Tassi2018-04-12 09:54:36 +0200
committerEnrico Tassi2018-04-12 09:54:36 +0200
commitd54b8dff818f0b1218df14cfb2b813da93154fa9 (patch)
treeb89257dd429d6d57c7efbe6403b9a231392b2a8b /htmldoc/buildlibgraph
parentc17414bbef21bb3d0b96ee004c29ef7d56e55e2e (diff)
remove ssrtest: it now belongs to Coq
Diffstat (limited to 'htmldoc/buildlibgraph')
-rwxr-xr-xhtmldoc/buildlibgraph2
1 files changed, 1 insertions, 1 deletions
diff --git a/htmldoc/buildlibgraph b/htmldoc/buildlibgraph
index 8544f1f..b7b91d0 100755
--- a/htmldoc/buildlibgraph
+++ b/htmldoc/buildlibgraph
@@ -157,6 +157,6 @@ for i=2,#arg do
end
_G[arg[1]]()
--- $COQBIN/coqdep -R . mathcomp */*.v | grep -v vio: | grep -v ssrtest > depend
+-- $COQBIN/coqdep -R . mathcomp */*.v | grep -v vio: > depend
-- cat depend | ./graph.lua dot | tee depend.dot | dot -T png -o depend.png
-- cat depend | ./graph.lua cytoscape `git show release/1.6:mathcomp/Make | grep 'v *$' | cut -d / -f 2 | cut -d . -f 1` > depend.js