equal
deleted
inserted
replaced
84 PDF=true |
84 PDF=true |
85 ;; |
85 ;; |
86 esac |
86 esac |
87 |
87 |
88 if [ -z "$OUTFILE" ]; then |
88 if [ -z "$OUTFILE" ]; then |
89 "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")" |
89 isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")" |
90 else |
90 else |
91 "$ISABELLE_TOOL" java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")" |
91 isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")" |
92 fi |
92 fi |
93 RC="$?" |
93 RC="$?" |
94 |
94 |
95 if [ -n "$PDF" ]; then |
95 if [ -n "$PDF" ]; then |
96 ( |
96 ( |
100 fi |
100 fi |
101 |
101 |
102 rm -f "$PRIVATE_FILE" |
102 rm -f "$PRIVATE_FILE" |
103 elif [ -z "$ADMIN_BUILD" ]; then |
103 elif [ -z "$ADMIN_BUILD" ]; then |
104 [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
104 [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
105 exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser |
105 exec isabelle java GraphBrowser.GraphBrowser |
106 else |
106 else |
107 RC=0 |
107 RC=0 |
108 fi |
108 fi |
109 |
109 |
110 exit "$RC" |
110 exit "$RC" |