From e5b94c29ff49f8b880290a72519157d26351bc6c Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 24 Dec 2010 23:49:15 +0000
Subject: Remove obsolete script univdot, update dev doc about universes

By the way, definitely remove "Dump Universes", which has been
deprecated since 2006 (r9306).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13754 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/tools/univdot | 49 -------------------------------------------------
 1 file changed, 49 deletions(-)
 delete mode 100755 dev/tools/univdot

(limited to 'dev/tools')

diff --git a/dev/tools/univdot b/dev/tools/univdot
deleted file mode 100755
index bb0dd2c89b..0000000000
--- a/dev/tools/univdot
+++ /dev/null
@@ -1,49 +0,0 @@
-#!/bin/sh
-
-usage() {
-    echo ""
-    echo "usage: univdot [INPUT] [OUTPUT]"
-    echo ""
-    echo "takes the output of Dump Universes \"file\" command"
-    echo "and transforms it to the dot format"
-    echo ""
-    echo "Coq> Dump Universes \"univ.raw\"."
-    echo ""
-    echo "user@host> univdot univ.raw | dot -Tps > univ.ps" 
-    echo ""
-}
-    
-
-# these are dot edge attributes to draw arrows corresponding 
-# to > >= and = edges of the universe graph
-
-GT="[color=red]"
-GE="[color=blue]"
-EQ="[color=black]"
-
-
-# input/output redirection
-case $# in
-  0) ;;
-  1) case $1 in
-       -h|-help|--help) usage
-               exit 0 ;;
-       *) exec < $1 ;;
-     esac ;;
-  2) exec < $1 > $2 ;;
-  *) usage
-     exit 0;;
-esac
-
-
-# dot header
-echo 'digraph G {\
-  size="7.5,10" ;\
-  rankdir = TB ;'
-
-sed -e "s/^\([^ =>]\+\) > \([^ =>]\+\)/\1 -> \2 $GT/" \
-      -e "s/^\([^ =>]\+\) >= \([^ =>]\+\)/\1 -> \2 $GE/" \
-      -e "s/^\([^ =>]\+\) = \([^ =>]\+\)/\1 -> \2 $EQ/" \
-| sed -e "s/\./_/g" 
-
-echo "}"
\ No newline at end of file
-- 
cgit v1.2.3