diff options
| author | Enrico Tassi | 2014-09-18 16:35:31 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-18 16:35:36 +0200 |
| commit | 870d81c699b5d15420a03f2006a7938a158c09a8 (patch) | |
| tree | 97c5bc27581d5c2e0ddd652ef7d569e4cf94d76e /dev/base_include | |
| parent | 854be50a06b1c0fd95a63402eeced0fd0388bf55 (diff) | |
mltop: when a plugin is loaded store its full path in the summary
This fixes the following bug related to stm: if one passes -I to coqide, then
such flag is passes to the workers; but if one uses "Add ML LoadPath" to
extend the paths in which coq looks for plugins, this extra path was
no passed to the slaves (via the command line) nor store in the system
state and hence sent to the slaves.
With this patch, when a cmxs is loaded, its full path is stored in the
summary and hence sent to the workers as one may expect.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions