Skip to content
Snippets Groups Projects
  • Virgile Prevosto's avatar
    211df542
    [script] Remove useless assignments · 211df542
    Virgile Prevosto authored
    - If FRAMAC_SHARE is not already set, either frama-c -print-share-path
      gives a correct result, and there's no need to set FRAMAC_SHARE in the
      first place, or it does not, and putting this result in FRAMAC_SHARE
      won't do any good.
    - there's no need (and it seems to confuse Frama-C) to -add-path when in
      internal mode.
    211df542
    History
    [script] Remove useless assignments
    Virgile Prevosto authored
    - If FRAMAC_SHARE is not already set, either frama-c -print-share-path
      gives a correct result, and there's no need to set FRAMAC_SHARE in the
      first place, or it does not, and putting this result in FRAMAC_SHARE
      won't do any good.
    - there's no need (and it seems to confuse Frama-C) to -add-path when in
      internal mode.