Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned comments;
  2. misc updates and clarification;
  3. clarified file name;
  4. merged
  5. updated to polyml-5.8.2 (official release);
  6. clarified default_platform_families (again);
  7. proper option for linux_arm;
  8. proper "$?";
Changeset 73647:a037f01aedab by wenzelm:
tuned comments;
The file was modified Admin/components/main (diff)
The file was modified Admin/components/optional (diff)
The file was modified Admin/components/windows (diff)
Changeset 73646:078ad17eb934 by wenzelm:
misc updates and clarification;
The file was modified Admin/components/PLATFORMS (diff)
Changeset 73645:dea7f6a2485e by wenzelm:
clarified file name;
The file was addedAdmin/components/PLATFORMS
The file was removedAdmin/PLATFORMS
Changeset 73644:0da9e824255f by wenzelm:
merged
Changeset 73643:9b4579e5bced by wenzelm:
updated to polyml-5.8.2 (official release);
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified Admin/polyml/README (diff)
Changeset 73642:ac6f8fff036b by wenzelm:
clarified default_platform_families (again);
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/System/platform.scala (diff)
Changeset 73641:a2d3b4a90bca by wenzelm:
proper option for linux_arm;
The file was modified Admin/etc/options (diff)
Changeset 73640:f4778e08dcd7 by wenzelm:
proper "$?";
The file was modified Admin/init (diff)