| changeset 44569 | 5130dfe1b7be |
| parent 44403 | 5aaa0fe92672 |
| child 45406 | 2f0a34fc4d2d |
| 44565:93dcfcf91484 | 44569:5130dfe1b7be |
|---|---|
200 |
200 |
201 # build |
201 # build |
202 |
202 |
203 if [ "$OUTDATED" = true ] |
203 if [ "$OUTDATED" = true ] |
204 then |
204 then |
205 echo "###" |
|
206 echo "### Building Isabelle/jEdit ..." |
205 echo "### Building Isabelle/jEdit ..." |
207 echo "###" |
|
208 |
206 |
209 [ "${#UPDATED[@]}" -gt 0 ] && { |
207 [ "${#UPDATED[@]}" -gt 0 ] && { |
210 echo "Changed files:" |
208 echo "Changed files:" |
211 for FILE in "${UPDATED[@]}" |
209 for FILE in "${UPDATED[@]}" |
212 do |
210 do |