← Back to branch summary

~tapaal-contributor/tapaal/change-export-batch-shortcut-1820012

« back to all changes in this revision

Viewing changes to src/pipe/gui/graphicElements/Place.java

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2019-03-13 07:17:48 UTC
  • mfrom: (989 tapaal)
  • mto: This revision was merged to the branch mainline in revision 991.
  • Revision ID: kenneth@yrke.dk-20190313071748-fm6dc00yy27un3xd
Merged with trunk

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/graphicElements/Place.java
19
19
 
20
20
        private static final long serialVersionUID = -5155964364065651381L;
21
21
 
 
22
 
22
23
        // Value of the capacity restriction; 0 means no capacity restriction 
23
24
        protected Integer capacity = 0;
24
25
 
159
160
        @Override
160
161
        public void update(boolean displayConstantNames) {
161
162
                if (attributesVisible) {
162
 
                        pnName.setText("\nk=" + (capacity > 0 ? capacity : "\u221E"));
 
163
                        pnName.setText("");
163
164
                } else {
164
165
                        pnName.setText("");
165
166
                }