diff options
| author | Pierre Courtieu | 2015-02-23 18:58:43 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2015-02-23 18:58:43 +0100 |
| commit | cea92f33654bf924f5be861a946ee5084eca840b (patch) | |
| tree | 97a825a97dd65a4d9d74b6870cc6396a1345901b /lib/cArray.ml | |
| parent | df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (diff) | |
Fixed 3233 (fresh does not work with a qualid).
fresh now accepts a qualid, and behaves as if given the short name.
Since fresh used to accept an id, supporting qualid is IMO not a new
feature but just a fix. Hence the fix in v8.5.
Diffstat (limited to 'lib/cArray.ml')
0 files changed, 0 insertions, 0 deletions